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  2373  axc10  2390  axc15  2427  sb2  2484  moim  2545  2eu6  2658  ral2imi  3077  ceqsalt  3464  spcimgft  3492  elabgtOLD  3616  elabgtOLDOLD  3617  sstr2  3929  ssralv  3991  difin0ss  4314  sepexlem  5234  axprlem2  5359  axprglem  5371  axnulg  35272  hbntg  36006  axtco2  36677  axnultcoreg  36683  bj-alsyl  36899  bj-2alim  36900  bj-alimdh  36901  bj-hbald  36989  bj-axc10v  37113  bj-sblem1  37162  bj-sblem2  37163  bj-ceqsalt0  37204  bj-ceqsalt1  37205  bj-axseprep  37394  wl-spae  37857  wl-aetr  37865  wl-axc11r  37866  wl-aleq  37871  wl-nfeqfb  37872  axc11-o  39408  pm10.57  44813  2al2imi  44815  19.41rg  44992  hbntal  44995