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  1920  aevlem0  2091  sbi1  2110  axc16g  2298  axc11r  2400  axc10  2417  axc15  2454  sb2  2511  moim  2572  2eu6  2684  ral2imi  3105  ceqsalt  3487  spcimgft  3514  elabgtOLD  3630  sstr2  3920  ssralv  3982  difin0ss  4324  sepexlem  5257  axprlem2  5390  axprglem  5398  axsepg2  35908  axsepg4  35911  axnulg  35913  axpowg2  35915  axpowg3  35916  hbntg  36745  axtco2  37440  axnulregtco  37446  bj-alsyl  37669  bj-2alim  37670  bj-alimdh  37671  bj-hbald  37759  bj-axc10v  37883  bj-sblem1  37932  bj-sblem2  37933  bj-ceqsalt0  37974  bj-ceqsalt1  37975  bj-axseprep  38181  wl-spae  38645  wl-aetr  38653  wl-axc11r  38654  wl-aleq  38659  wl-nfeqfb  38660  axc11-o  40200  pm10.57  45547  2al2imi  45549  19.41rg  45724  hbntal  45727  quantgodelALT  48090