Theorem al2imi 1848

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1828  ax-4 1842

This theorem is used by:  alanimi  1849  alimdh  1850  albi  1851  aleximi  1865  19.33b  1918  aevlem0  2089  sbi1  2108  axc16g  2295  axc11r  2398  axc10  2415  axc15  2452  sb2  2509  moim  2570  2eu6  2682  ral2imi  3102  ceqsalt  3484  spcimgft  3511  elabgtOLD  3627  sstr2  3938  ssralv  4000  difin0ss  4321  sepexlem  5254  axprlem2  5386  axprglem  5394  axsepg2  35781  axsepg4  35784  axnulg  35786  axpowg2  35788  axpowg3  35789  hbntg  36537  axtco2  37232  axnulregtco  37238  bj-alsyl  37461  bj-2alim  37462  bj-alimdh  37463  bj-hbald  37551  bj-axc10v  37675  bj-sblem1  37724  bj-sblem2  37725  bj-ceqsalt0  37766  bj-ceqsalt1  37767  bj-axseprep  37958  wl-spae  38421  wl-aetr  38429  wl-axc11r  38430  wl-aleq  38435  wl-nfeqfb  38436  axc11-o  39976  pm10.57  45314  2al2imi  45316  19.41rg  45492  hbntal  45495  quantgodelALT  47829