Metamath Proof Explorer


Theorem vtoclgftOLD

Description: Obsolete version of vtoclgft . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion vtoclgftOLD _ x A x ψ x x = A φ ψ x φ A V ψ

Proof

Step Hyp Ref Expression
1 elisset A V z z = A
2 nfnfc1 x _ x A
3 nfcvd _ x A _ x z
4 id _ x A _ x A
5 3 4 nfeqd _ x A x z = A
6 eqeq1 z = x z = A x = A
7 6 a1i _ x A z = x z = A x = A
8 2 5 7 cbvexd _ x A z z = A x x = A
9 1 8 syl5ib _ x A A V x x = A
10 9 ad2antrr _ x A x ψ x x = A φ ψ x φ A V x x = A
11 10 3impia _ x A x ψ x x = A φ ψ x φ A V x x = A
12 biimp φ ψ φ ψ
13 12 imim2i x = A φ ψ x = A φ ψ
14 13 com23 x = A φ ψ φ x = A ψ
15 14 imp x = A φ ψ φ x = A ψ
16 15 alanimi x x = A φ ψ x φ x x = A ψ
17 19.23t x ψ x x = A ψ x x = A ψ
18 17 adantl _ x A x ψ x x = A ψ x x = A ψ
19 16 18 syl5ib _ x A x ψ x x = A φ ψ x φ x x = A ψ
20 19 imp _ x A x ψ x x = A φ ψ x φ x x = A ψ
21 20 3adant3 _ x A x ψ x x = A φ ψ x φ A V x x = A ψ
22 11 21 mpd _ x A x ψ x x = A φ ψ x φ A V ψ