Theorem al2imi 1847

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1827  ax-4 1841

This theorem is used by:  alanimi  1848  alimdh  1849  albi  1850  aleximi  1864  19.33b  1917  aevlem0  2088  sbi1  2107  axc16g  2294  axc11r  2397  axc10  2414  axc15  2451  sb2  2508  moim  2569  2eu6  2681  ral2imi  3101  ceqsalt  3483  spcimgft  3510  elabgtOLD  3626  sstr2  3915  ssralv  3977  difin0ss  4320  sepexlem  5253  axprlem2  5385  axprglem  5393  axsepg2  35851  axsepg4  35854  axnulg  35856  axpowg2  35858  axpowg3  35859  hbntg  36610  axtco2  37305  axnulregtco  37311  bj-alsyl  37534  bj-2alim  37535  bj-alimdh  37536  bj-hbald  37624  bj-axc10v  37748  bj-sblem1  37797  bj-sblem2  37798  bj-ceqsalt0  37839  bj-ceqsalt1  37840  bj-axseprep  38033  wl-spae  38497  wl-aetr  38505  wl-axc11r  38506  wl-aleq  38511  wl-nfeqfb  38512  axc11-o  40052  pm10.57  45399  2al2imi  45401  19.41rg  45577  hbntal  45580  quantgodelALT  47929