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 ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ∀ 𝑥 ( ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )

Proof

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