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  2367  axc10  2384  axc15  2421  sb2  2478  moim  2538  2eu6  2651  ral2imi  3069  ceqsalt  3484  spcimgft  3515  elabgt  3641  elabgtOLD  3642  sstr2  3955  ssralv  4017  difin0ss  4338  sepexlem  5256  axprlem2  5381  axnulg  35088  hbntg  35788  bj-2alim  36593  bj-cbvalimt  36622  bj-axc10v  36776  bj-sblem1  36825  bj-sblem2  36826  bj-ceqsalt0  36867  bj-ceqsalt1  36868  wl-spae  37504  wl-aetr  37512  wl-axc11r  37513  wl-aleq  37518  wl-nfeqfb  37519  axc11-o  38939  pm10.57  44353  2al2imi  44355  19.41rg  44533  hbntal  44536