Theorem al2imi 1822

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

Syntax hints:   → wi 4  ∀wal 1545

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

This theorem is referenced by:  alanimi  1823  alimdh  1824  albi  1825  aleximi  1839  19.33b  1892  aevlem0  2063  sbi1  2082  axc16g  2272  axc11r  2376  axc10  2393  axc15  2430  sb2  2487  moim  2548  2eu6  2661  ral2imi  3079  ceqsalt  3466  spcimgft  3494  elabgtOLD  3618  sstr2  3929  ssralv  3990  difin0ss  4308  sepexlem  5228  axprlem2  5360  axprglem  5372  axsepg2  35328  axsepg4  35331  axnulg  35333  axpowg2  35335  axpowg3  35336  hbntg  36038  axtco2  36709  axnulregtco  36715  bj-alsyl  36939  bj-2alim  36940  bj-alimdh  36941  bj-hbald  37029  bj-axc10v  37153  bj-sblem1  37202  bj-sblem2  37203  bj-ceqsalt0  37244  bj-ceqsalt1  37245  bj-axseprep  37434  wl-spae  37899  wl-aetr  37907  wl-axc11r  37908  wl-aleq  37913  wl-nfeqfb  37914  axc11-o  39450  pm10.57  44822  2al2imi  44824  19.41rg  45001  hbntal  45004  quantgodelALT  47325