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