This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2pm13.193

Description: pm13.193 for two variables. pm13.193 is Theorem *13.193 in WhiteheadRussell p. 179. Derived from 2pm13.193VD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 simpll ⊢ x = u ∧ y = v ∧ u x v y φ → x = u
2 simplr ⊢ x = u ∧ y = v ∧ u x v y φ → y = v
3 simpr ⊢ x = u ∧ y = v ∧ u x v y φ → u x v y φ
4 sbequ2 ⊢ x = u → u x v y φ → v y φ
5 1 3 4 sylc ⊢ x = u ∧ y = v ∧ u x v y φ → v y φ
6 sbequ2 ⊢ y = v → v y φ → φ
7 2 5 6 sylc ⊢ x = u ∧ y = v ∧ u x v y φ → φ
8 1 2 7 jca31 ⊢ x = u ∧ y = v ∧ u x v y φ → x = u ∧ y = v ∧ φ
9 simpll ⊢ x = u ∧ y = v ∧ φ → x = u
10 simplr ⊢ x = u ∧ y = v ∧ φ → y = v
11 simpr ⊢ x = u ∧ y = v ∧ φ → φ
12 sbequ1 ⊢ y = v → φ → v y φ
13 10 11 12 sylc ⊢ x = u ∧ y = v ∧ φ → v y φ
14 sbequ1 ⊢ x = u → v y φ → u x v y φ
15 9 13 14 sylc ⊢ x = u ∧ y = v ∧ φ → u x v y φ
16 9 10 15 jca31 ⊢ x = u ∧ y = v ∧ φ → x = u ∧ y = v ∧ u x v y φ
17 8 16 impbii ⊢ x = u ∧ y = v ∧ u x v y φ ↔ x = u ∧ y = v ∧ φ