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  2371  axc10  2390  axc15  2427  sb2  2484  moim  2544  2eu6  2657  ral2imi  3076  ceqsalt  3499  spcimgft  3530  elabgt  3656  elabgtOLD  3657  sstr2  3970  ssralv  4032  difin0ss  4353  sepexlem  5274  axprlem2  5399  axnulg  35128  hbntg  35828  bj-2alim  36633  bj-cbvalimt  36662  bj-axc10v  36816  bj-sblem1  36865  bj-sblem2  36866  bj-ceqsalt0  36907  bj-ceqsalt1  36908  wl-spae  37544  wl-aetr  37552  wl-axc11r  37553  wl-aleq  37558  wl-nfeqfb  37559  axc11-o  38974  pm10.57  44362  2al2imi  44364  19.41rg  44542  hbntal  44545