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  2299  axc11r  2403  axc10  2420  axc15  2457  sb2  2514  moim  2575  2eu6  2687  ral2imi  3107  ceqsalt  3491  spcimgft  3518  elabgtOLD  3635  sstr2  3947  ssralv  4009  difin0ss  4331  sepexlem  5267  axprlem2  5400  axprglem  5412  axsepg2  35577  axsepg4  35580  axnulg  35582  axpowg2  35584  axpowg3  35585  hbntg  36316  axtco2  37026  axnulregtco  37032  bj-alsyl  37255  bj-2alim  37256  bj-alimdh  37257  bj-hbald  37345  bj-axc10v  37469  bj-sblem1  37518  bj-sblem2  37519  bj-ceqsalt0  37560  bj-ceqsalt1  37561  bj-axseprep  37752  wl-spae  38217  wl-aetr  38225  wl-axc11r  38226  wl-aleq  38231  wl-nfeqfb  38232  axc11-o  39766  pm10.57  45122  2al2imi  45124  19.41rg  45300  hbntal  45303  quantgodelALT  47630