Theorem al2imi 1817

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  alanimi  1818  alimdh  1819  albi  1820  aleximi  1834  19.33b  1887  aevlem0  2058  sbi1  2077  axc16g  2268  axc11r  2372  axc10  2389  axc15  2426  sb2  2483  moim  2544  2eu6  2657  ral2imi  3076  ceqsalt  3463  spcimgft  3491  elabgtOLD  3615  elabgtOLDOLD  3616  sstr2  3928  ssralv  3990  difin0ss  4313  sepexlem  5234  axprlem2  5366  axprglem  5378  axnulg  35251  hbntg  35985  axtco2  36656  axnulregtco  36662  bj-alsyl  36886  bj-2alim  36887  bj-alimdh  36888  bj-hbald  36976  bj-axc10v  37100  bj-sblem1  37149  bj-sblem2  37150  bj-ceqsalt0  37191  bj-ceqsalt1  37192  bj-axseprep  37381  wl-spae  37846  wl-aetr  37854  wl-axc11r  37855  wl-aleq  37860  wl-nfeqfb  37861  axc11-o  39397  pm10.57  44798  2al2imi  44800  19.41rg  44977  hbntal  44980  quantgodelALT  47303