Metamath Proof Explorer


Theorem hbimpgVD

Description: Virtual deduction proof of hbimpg . 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. hbimpg is hbimpgVD without virtual deductions and was automatically derived from hbimpgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ).
2:1: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ph -> A. x ph ) ).
3:: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) , -. ph ->. -. ph ).
4:2: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( -. ph -> A. x -. ph ) ).
5:4: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x -. ph ) ).
6:3,5: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) , -. ph ->. A. x -. ph ).
7:: |- ( -. ph -> ( ph -> ps ) )
8:7: |- ( A. x -. ph -> A. x ( ph -> ps ) )
9:6,8: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) , -. ph ->. A. x ( ph -> ps ) ).
10:9: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( -. ph -> A. x ( ph -> ps ) ) ).
11:: |- ( ps -> ( ph -> ps ) )
12:11: |- ( A. x ps -> A. x ( ph -> ps ) )
13:1: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ps -> A. x ps ) ).
14:13: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ps ) ).
15:14,12: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ps -> A. x ( ph -> ps ) ) ).
16:10,15: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ).
17:: |- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
18:16,17: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
19:: |- ( A. x ( ph -> A. x ph ) -> A. x A. x ( ph -> A. x ph ) )
20:: |- ( A. x ( ps -> A. x ps ) -> A. x A. x ( ps -> A. x ps ) )
21:19,20: |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) )
22:21,18: |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) ->. A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
qed:22: |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps -> A. x ps ) ) -> A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) )

Ref Expression
Assertion hbimpgVD xφxφxψxψxφψxφψ

Proof

Step Hyp Ref Expression
1 hba1 xφxφxxφxφ
2 hba1 xψxψxxψxψ
3 1 2 hban xφxφxψxψxxφxφxψxψ
4 idn2 xφxφxψxψ,¬φ¬φ
5 idn1 xφxφxψxψxφxφxψxψ
6 simpl xφxφxψxψxφxφ
7 5 6 e1a xφxφxψxψxφxφ
8 hbntal xφxφx¬φx¬φ
9 7 8 e1a xφxφxψxψx¬φx¬φ
10 sp x¬φx¬φ¬φx¬φ
11 9 10 e1a xφxφxψxψ¬φx¬φ
12 pm2.27 ¬φ¬φx¬φx¬φ
13 4 11 12 e21 xφxφxψxψ,¬φx¬φ
14 pm2.21 ¬φφψ
15 14 alimi x¬φxφψ
16 13 15 e2 xφxφxψxψ,¬φxφψ
17 16 in2 xφxφxψxψ¬φxφψ
18 simpr xφxφxψxψxψxψ
19 5 18 e1a xφxφxψxψxψxψ
20 sp xψxψψxψ
21 19 20 e1a xφxφxψxψψxψ
22 ax-1 ψφψ
23 22 alimi xψxφψ
24 imim1 ψxψxψxφψψxφψ
25 21 23 24 e10 xφxφxψxψψxφψ
26 jao ¬φxφψψxφψ¬φψxφψ
27 17 25 26 e11 xφxφxψxψ¬φψxφψ
28 imor φψ¬φψ
29 imbi1 φψ¬φψφψxφψ¬φψxφψ
30 29 biimprcd ¬φψxφψφψ¬φψφψxφψ
31 27 28 30 e10 xφxφxψxψφψxφψ
32 3 31 gen11nv xφxφxψxψxφψxφψ
33 32 in1 xφxφxψxψxφψxφψ