Theorem al2imi 1778

Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
al2imi.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
al2imi	⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Proof of Theorem al2imi

Step	Hyp	Ref	Expression
1		al2im 1777	. 2 ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2		al2imi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	mpg 1760	1 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1758  ax-4 1772

This theorem is referenced by:  alanimi  1779  alimdh  1780  albi  1781  aleximi  1794  19.33b  1848  aevlem0  2003  sbi1  2022  axc16g  2187  sbi1vOLD  2246  axc11r  2300  axc10  2315  axc15  2357  sb2  2424  sbequiOLD  2455  sbi1OLD  2463  sbequiALT  2523  sbi1ALT  2533  moim  2552  2eu6  2689  ral2imi  3107  ceqsalt  3449  difin0ss  4215  axprlem2  5181  hbntg  32568  bj-2alim  33457  bj-cbvalimt  33480  bj-axc10v  33567  bj-sblem1  33654  bj-sblem2  33655  bj-ceqsalt0  33690  bj-ceqsalt1  33691  wl-spae  34201  wl-aetr  34209  wl-aleq  34214  wl-nfeqfb  34215  axc11-o  35529  pm10.57  40116  2al2imi  40118  19.41rg  40300  hbntal  40303