Theorem al2imi 1816

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

Syntax hints:   → wi 4  ∀wal 1539

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

This theorem is referenced by:  alanimi  1817  alimdh  1818  albi  1819  aleximi  1833  19.33b  1886  aevlem0  2057  sbi1  2076  axc16g  2267  axc11r  2372  axc10  2389  axc15  2426  sb2  2483  moim  2544  2eu6  2657  ral2imi  3075  ceqsalt  3474  spcimgft  3503  elabgtOLD  3627  elabgtOLDOLD  3628  sstr2  3940  ssralv  4002  difin0ss  4325  sepexlem  5244  axprlem2  5369  axnulg  35264  hbntg  35997  bj-2alim  36810  bj-cbvalimt  36839  bj-axc10v  36994  bj-sblem1  37043  bj-sblem2  37044  bj-ceqsalt0  37085  bj-ceqsalt1  37086  wl-spae  37722  wl-aetr  37730  wl-axc11r  37731  wl-aleq  37736  wl-nfeqfb  37737  axc11-o  39207  pm10.57  44608  2al2imi  44610  19.41rg  44787  hbntal  44790