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  2366  axc10  2383  axc15  2420  sb2  2477  moim  2537  2eu6  2650  ral2imi  3068  ceqsalt  3472  spcimgft  3503  elabgtOLD  3630  elabgtOLDOLD  3631  sstr2  3944  ssralv  4006  difin0ss  4326  sepexlem  5241  axprlem2  5366  axnulg  35058  hbntg  35778  bj-2alim  36583  bj-cbvalimt  36612  bj-axc10v  36766  bj-sblem1  36815  bj-sblem2  36816  bj-ceqsalt0  36857  bj-ceqsalt1  36858  wl-spae  37494  wl-aetr  37502  wl-axc11r  37503  wl-aleq  37508  wl-nfeqfb  37509  axc11-o  38929  pm10.57  44344  2al2imi  44346  19.41rg  44524  hbntal  44527