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  3476  spcimgft  3505  elabgtOLD  3629  elabgtOLDOLD  3630  sstr2  3942  ssralv  4004  difin0ss  4327  sepexlem  5246  axprlem2  5371  axprglem  5382  axnulg  35283  hbntg  36016  bj-alsyl  36836  bj-2alim  36837  bj-cbvalimt  36869  bj-axc10v  37035  bj-sblem1  37084  bj-sblem2  37085  bj-ceqsalt0  37126  bj-ceqsalt1  37127  bj-axseprep  37316  wl-spae  37770  wl-aetr  37778  wl-axc11r  37779  wl-aleq  37784  wl-nfeqfb  37785  axc11-o  39321  pm10.57  44721  2al2imi  44723  19.41rg  44900  hbntal  44903