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  2296  axc11r  2399  axc10  2416  axc15  2453  sb2  2510  moim  2571  2eu6  2683  ral2imi  3103  ceqsalt  3486  spcimgft  3513  elabgtOLD  3630  sstr2  3941  ssralv  4003  difin0ss  4324  sepexlem  5260  axprlem2  5393  axprglem  5405  axsepg2  35674  axsepg4  35677  axnulg  35679  axpowg2  35681  axpowg3  35682  hbntg  36390  axtco2  37101  axnulregtco  37107  bj-alsyl  37330  bj-2alim  37331  bj-alimdh  37332  bj-hbald  37420  bj-axc10v  37544  bj-sblem1  37593  bj-sblem2  37594  bj-ceqsalt0  37635  bj-ceqsalt1  37636  bj-axseprep  37827  wl-spae  38292  wl-aetr  38300  wl-axc11r  38301  wl-aleq  38306  wl-nfeqfb  38307  axc11-o  39832  pm10.57  45203  2al2imi  45205  19.41rg  45381  hbntal  45384  quantgodelALT  47711