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.}
[2] (Connected (In 1 C1) (In 1 X1)) {Given}
[3] (Signal (In 1 C1) (Signal (In 1 X1))) {[1],[2]: Gen. Modus Ponens}
[4] (Function Signal) {Given}
[5] (Signal (In 1 C1) On) {Given}
[6] (= (Signal (In 1 X1)) On) {[3],[4],[5]: Fun. Val. Equiv.}
[11] (= (Signal (In 2 X1)) On) {[8],[9],[10]: Fun. Val. Equiv.}
[12] (= (Signal (In 1 X1) On) (Signal (In 2 X1) On)) {[6],[11]: Trans. Of =}