Metamath Proof Explorer

Theorem 2pm13.193VD

Description: Virtual deduction proof of 2pm13.193 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. 2pm13.193 is 2pm13.193VD without virtual deductions and was automatically derived from 2pm13.193VD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
2:1: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( x = u /\ y = v ) ).
3:2: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. x = u ).
4:1: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ u / x ] [ v / y ] ph ).
5:3,4: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
6:5: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ x = u ) ).
7:6: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ v / y ] ph ).
8:2: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. y = v ).
9:7,8: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ y = v ) ).
10:9: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ph /\ y = v ) ).
11:10: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ph ).
12:2,11: |- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
13:12: |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> ( ( x = u /\ y = v ) /\ ph ) )
14:: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
15:14: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( x = u /\ y = v ) ).
16:15: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. y = v ).
17:14: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ph ).
18:16,17: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ph /\ y = v ) ).
19:18: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ y = v ) ).
20:15: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. x = u ).
21:19: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. [ v / y ] ph ).
22:20,21: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ x = u ) ).
23:22: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
24:23: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. [ u / x ] [ v / y ] ph ).
25:15,24: |- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
26:25: |- ( ( ( x = u /\ y = v ) /\ ph ) -> ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
qed:13,26: |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )

Ref Expression
Assertion 2pm13.193VD ⊢ x = u ∧ y = v ∧ u x v y φ ↔ x = u ∧ y = v ∧ φ

Proof

Step Hyp Ref Expression
1 idn1 ⊢ x = u ∧ y = v ∧ u x v y φ → x = u ∧ y = v ∧ u x v y φ
2 simpl ⊢ x = u ∧ y = v ∧ u x v y φ → x = u ∧ y = v
3 1 2 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → x = u ∧ y = v
4 simpl ⊢ x = u ∧ y = v → x = u
5 3 4 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → x = u
6 simpr ⊢ x = u ∧ y = v ∧ u x v y φ → u x v y φ
7 1 6 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → u x v y φ
8 pm3.21 ⊢ x = u → u x v y φ → u x v y φ ∧ x = u
9 5 7 8 e11 ⊢ x = u ∧ y = v ∧ u x v y φ → u x v y φ ∧ x = u
10 sbequ2 ⊢ x = u → u x v y φ → v y φ
11 10 imdistanri ⊢ u x v y φ ∧ x = u → v y φ ∧ x = u
12 9 11 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → v y φ ∧ x = u
13 simpl ⊢ v y φ ∧ x = u → v y φ
14 12 13 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → v y φ
15 simpr ⊢ x = u ∧ y = v → y = v
16 3 15 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → y = v
17 pm3.2 ⊢ v y φ → y = v → v y φ ∧ y = v
18 14 16 17 e11 ⊢ x = u ∧ y = v ∧ u x v y φ → v y φ ∧ y = v
19 sbequ2 ⊢ y = v → v y φ → φ
20 19 imdistanri ⊢ v y φ ∧ y = v → φ ∧ y = v
21 18 20 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → φ ∧ y = v
22 simpl ⊢ φ ∧ y = v → φ
23 21 22 e1a ⊢ x = u ∧ y = v ∧ u x v y φ → φ
24 pm3.2 ⊢ x = u ∧ y = v → φ → x = u ∧ y = v ∧ φ
25 3 23 24 e11 ⊢ x = u ∧ y = v ∧ u x v y φ → x = u ∧ y = v ∧ φ
26 25 in1 ⊢ x = u ∧ y = v ∧ u x v y φ → x = u ∧ y = v ∧ φ
27 idn1 ⊢ x = u ∧ y = v ∧ φ → x = u ∧ y = v ∧ φ
28 simpl ⊢ x = u ∧ y = v ∧ φ → x = u ∧ y = v
29 27 28 e1a ⊢ x = u ∧ y = v ∧ φ → x = u ∧ y = v
30 29 4 e1a ⊢ x = u ∧ y = v ∧ φ → x = u
31 29 15 e1a ⊢ x = u ∧ y = v ∧ φ → y = v
32 simpr ⊢ x = u ∧ y = v ∧ φ → φ
33 27 32 e1a ⊢ x = u ∧ y = v ∧ φ → φ
34 pm3.21 ⊢ y = v → φ → φ ∧ y = v
35 31 33 34 e11 ⊢ x = u ∧ y = v ∧ φ → φ ∧ y = v
36 sbequ1 ⊢ y = v → φ → v y φ
37 36 imdistanri ⊢ φ ∧ y = v → v y φ ∧ y = v
38 35 37 e1a ⊢ x = u ∧ y = v ∧ φ → v y φ ∧ y = v
39 simpl ⊢ v y φ ∧ y = v → v y φ
40 38 39 e1a ⊢ x = u ∧ y = v ∧ φ → v y φ
41 pm3.21 ⊢ x = u → v y φ → v y φ ∧ x = u
42 30 40 41 e11 ⊢ x = u ∧ y = v ∧ φ → v y φ ∧ x = u
43 sbequ1 ⊢ x = u → v y φ → u x v y φ
44 43 imdistanri ⊢ v y φ ∧ x = u → u x v y φ ∧ x = u
45 42 44 e1a ⊢ x = u ∧ y = v ∧ φ → u x v y φ ∧ x = u
46 simpl ⊢ u x v y φ ∧ x = u → u x v y φ
47 45 46 e1a ⊢ x = u ∧ y = v ∧ φ → u x v y φ
48 pm3.2 ⊢ x = u ∧ y = v → u x v y φ → x = u ∧ y = v ∧ u x v y φ
49 29 47 48 e11 ⊢ x = u ∧ y = v ∧ φ → x = u ∧ y = v ∧ u x v y φ
50 49 in1 ⊢ x = u ∧ y = v ∧ φ → x = u ∧ y = v ∧ u x v y φ
51 26 50 impbii ⊢ x = u ∧ y = v ∧ u x v y φ ↔ x = u ∧ y = v ∧ φ