Theorem al2imi 1845

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

Syntax hints:   → wi 4  ∀wal 1568

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

This theorem is referenced by:  alanimi  1846  alimdh  1847  albi  1848  aleximi  1862  19.33b  1915  aevlem0  2086  sbi1  2105  axc16g  2296  axc11r  2400  axc10  2417  axc15  2454  sb2  2511  moim  2572  2eu6  2684  ral2imi  3104  ceqsalt  3488  spcimgft  3515  elabgtOLD  3633  sstr2  3945  ssralv  4007  difin0ss  4329  sepexlem  5263  axprlem2  5397  axprglem  5409  axsepg2  35531  axsepg4  35534  axnulg  35536  axpowg2  35538  axpowg3  35539  hbntg  36273  axtco2  36963  axnulregtco  36969  bj-alsyl  37192  bj-2alim  37193  bj-alimdh  37194  bj-hbald  37282  bj-axc10v  37406  bj-sblem1  37455  bj-sblem2  37456  bj-ceqsalt0  37497  bj-ceqsalt1  37498  bj-axseprep  37689  wl-spae  38154  wl-aetr  38162  wl-axc11r  38163  wl-aleq  38168  wl-nfeqfb  38169  axc11-o  39703  pm10.57  45061  2al2imi  45063  19.41rg  45239  hbntal  45242  quantgodelALT  47569