Theorem al2imi 1813

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 1812	. 2 ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2		al2imi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	mpg 1795	1 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1793  ax-4 1807

This theorem is referenced by:  alanimi  1814  alimdh  1815  albi  1816  aleximi  1830  19.33b  1884  aevlem0  2054  sbi1  2071  axc16g  2261  axc11r  2374  axc10  2393  axc15  2430  sb2  2487  moim  2547  2eu6  2660  ral2imi  3091  ceqsalt  3523  spcimgft  3558  elabgt  3685  elabgtOLD  3686  sstr2  4015  ssralv  4077  difin0ss  4396  axprlem2  5442  axnulg  35068  hbntg  35769  bj-2alim  36576  bj-cbvalimt  36605  bj-axc10v  36759  bj-sblem1  36808  bj-sblem2  36809  bj-ceqsalt0  36850  bj-ceqsalt1  36851  wl-spae  37475  wl-aetr  37483  wl-axc11r  37484  wl-aleq  37489  wl-nfeqfb  37490  axc11-o  38907  pm10.57  44340  2al2imi  44342  19.41rg  44521  hbntal  44524