Theorem al2imi 1815

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

Syntax hints:   → wi 4  ∀wal 1538

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

This theorem is referenced by:  alanimi  1816  alimdh  1817  albi  1818  aleximi  1832  19.33b  1885  aevlem0  2055  sbi1  2072  axc16g  2261  axc11r  2366  axc10  2383  axc15  2420  sb2  2477  moim  2537  2eu6  2650  ral2imi  3068  ceqsalt  3481  spcimgft  3512  elabgtOLD  3639  elabgtOLDOLD  3640  sstr2  3953  ssralv  4015  difin0ss  4336  sepexlem  5254  axprlem2  5379  axnulg  35082  hbntg  35793  bj-2alim  36598  bj-cbvalimt  36627  bj-axc10v  36781  bj-sblem1  36830  bj-sblem2  36831  bj-ceqsalt0  36872  bj-ceqsalt1  36873  wl-spae  37509  wl-aetr  37517  wl-axc11r  37518  wl-aleq  37523  wl-nfeqfb  37524  axc11-o  38944  pm10.57  44360  2al2imi  44362  19.41rg  44540  hbntal  44543