Metamath Proof Explorer


Theorem elex22VD

Description: Virtual deduction proof of elex22 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elex22VD ABACxxBxC

Proof

Step Hyp Ref Expression
1 idn1 ABACABAC
2 simpl ABACAB
3 1 2 e1a ABACAB
4 elisset ABxx=A
5 3 4 e1a ABACxx=A
6 idn2 ABAC,x=Ax=A
7 eleq1a ABx=AxB
8 3 6 7 e12 ABAC,x=AxB
9 simpr ABACAC
10 1 9 e1a ABACAC
11 eleq1a ACx=AxC
12 10 6 11 e12 ABAC,x=AxC
13 pm3.2 xBxCxBxC
14 8 12 13 e22 ABAC,x=AxBxC
15 14 in2 ABACx=AxBxC
16 15 gen11 ABACxx=AxBxC
17 exim xx=AxBxCxx=AxxBxC
18 16 17 e1a ABACxx=AxxBxC
19 pm2.27 xx=Axx=AxxBxCxxBxC
20 5 18 19 e11 ABACxxBxC
21 20 in1 ABACxxBxC