Metamath Proof Explorer


Theorem ceqsalt

Description: Closed theorem version of ceqsalg . (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 10-Oct-2016)

Ref Expression
Assertion ceqsalt xψxx=AφψAVxx=Aφψ

Proof

Step Hyp Ref Expression
1 elisset AVxx=A
2 1 3ad2ant3 xψxx=AφψAVxx=A
3 biimp φψφψ
4 3 imim3i x=Aφψx=Aφx=Aψ
5 4 al2imi xx=Aφψxx=Aφxx=Aψ
6 5 3ad2ant2 xψxx=AφψAVxx=Aφxx=Aψ
7 19.23t xψxx=Aψxx=Aψ
8 7 3ad2ant1 xψxx=AφψAVxx=Aψxx=Aψ
9 6 8 sylibd xψxx=AφψAVxx=Aφxx=Aψ
10 2 9 mpid xψxx=AφψAVxx=Aφψ
11 biimpr φψψφ
12 11 imim2i x=Aφψx=Aψφ
13 12 com23 x=Aφψψx=Aφ
14 13 alimi xx=Aφψxψx=Aφ
15 14 3ad2ant2 xψxx=AφψAVxψx=Aφ
16 19.21t xψxψx=Aφψxx=Aφ
17 16 3ad2ant1 xψxx=AφψAVxψx=Aφψxx=Aφ
18 15 17 mpbid xψxx=AφψAVψxx=Aφ
19 10 18 impbid xψxx=AφψAVxx=Aφψ