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 1535

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  1832  19.33b  1886  aevlem0  2059  sbi1  2076  axc16g  2261  sbi1vOLD  2323  axc11r  2386  axc10  2403  axc15  2444  sb2  2504  sbequiOLD  2534  sbi1OLD  2542  sbequiALT  2596  sbi1ALT  2606  moim  2626  2eu6  2742  ral2imi  3158  ceqsalt  3529  difin0ss  4330  axprlem2  5327  hbntg  33052  bj-2alim  33946  bj-cbvalimt  33974  bj-axc10v  34117  bj-sblem1  34168  bj-sblem2  34169  bj-ceqsalt0  34202  bj-ceqsalt1  34203  wl-spae  34763  wl-aetr  34771  wl-axc11r  34772  wl-aleq  34777  wl-nfeqfb  34778  axc11-o  36089  pm10.57  40710  2al2imi  40712  19.41rg  40891  hbntal  40894