The Inputs of X1 are Equal
[1] (=> (Connected ?t1 ?t2)
(= (Signal ?t1) (Signal ?t2))) {Given}
[2] (=> (Connected (In 1 C1) (In 1 X1))
(= (Signal (In 1 C1)) (Signal (In 1 X1)))) {[1]: Univ. Elim.}
[3] (Connected (In 1 C1) (In 1 X1)) {Given}
[4] (= (Signal (In 1 C1)) (Signal (In 1 X1))) {[1],[3]: Gen. Modus Ponens}
[5] (= (Signal (In 1 C1)) On) {Given}
[6] (= (Signal (In 1 X1)) On) {[4],[5]: Trans. Of =}
[12] (= (Signal (In 2 X1)) On) {[10],[11]: Trans. Of =}
[13] (= (Signal (In 1 X1)) (Signal (In 2 X1))) {[6],[12]: Trans. Of =}