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  2074  axc16g  2263  axc11r  2368  axc10  2385  axc15  2422  sb2  2479  moim  2539  2eu6  2652  ral2imi  3071  ceqsalt  3470  spcimgft  3501  elabgtOLD  3628  elabgtOLDOLD  3629  sstr2  3941  ssralv  4003  difin0ss  4323  sepexlem  5237  axprlem2  5362  axnulg  35110  hbntg  35838  bj-2alim  36643  bj-cbvalimt  36672  bj-axc10v  36826  bj-sblem1  36875  bj-sblem2  36876  bj-ceqsalt0  36917  bj-ceqsalt1  36918  wl-spae  37554  wl-aetr  37562  wl-axc11r  37563  wl-aleq  37568  wl-nfeqfb  37569  axc11-o  38989  pm10.57  44403  2al2imi  44405  19.41rg  44582  hbntal  44585