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  elabgtOLD  3642  elabgtOLDOLD  3643  sstr2  3956  ssralv  4018  difin0ss  4339  sepexlem  5257  axprlem2  5382  axnulg  35089  hbntg  35800  bj-2alim  36605  bj-cbvalimt  36634  bj-axc10v  36788  bj-sblem1  36837  bj-sblem2  36838  bj-ceqsalt0  36879  bj-ceqsalt1  36880  wl-spae  37516  wl-aetr  37524  wl-axc11r  37525  wl-aleq  37530  wl-nfeqfb  37531  axc11-o  38951  pm10.57  44367  2al2imi  44369  19.41rg  44547  hbntal  44550