Theorem al2imi 1838

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 1837	. 2 ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2		al2imi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	mpg 1820	1 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1561

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

This theorem is referenced by:  alanimi  1839  alimdh  1840  albi  1841  aleximi  1855  19.33b  1908  aevlem0  2079  sbi1lem  2105  sbi1ALT  2107  axc16g  2298  axc11r  2402  axc10  2419  axc15  2456  sb2  2513  moim  2574  2eu6  2686  ral2imi  3104  ceqsalt  3490  spcimgft  3517  elabgtOLD  3635  sstr2  3946  ssralv  4008  difin0ss  4329  sepexlem  5254  axprlem2  5386  axprglem  5398  axsepg2  35448  axsepg4  35451  axnulg  35453  axpowg2  35455  axpowg3  35456  hbntg  36166  axtco2  36847  axnulregtco  36853  bj-alsyl  37076  bj-2alim  37077  bj-alimdh  37078  bj-hbald  37166  bj-axc10v  37290  bj-sblem1  37339  bj-sblem2  37340  bj-ceqsalt0  37381  bj-ceqsalt1  37382  bj-axseprep  37571  wl-spae  38036  wl-aetr  38044  wl-axc11r  38045  wl-aleq  38050  wl-nfeqfb  38051  axc11-o  39587  pm10.57  44945  2al2imi  44947  19.41rg  45124  hbntal  45127  quantgodelALT  47447