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  35864  axsepg4  35867  axnulg  35869  axpowg2  35871  axpowg3  35872  hbntg  36659  axtco2  37354  axnulregtco  37360  bj-alsyl  37583  bj-2alim  37584  bj-alimdh  37585  bj-hbald  37673  bj-axc10v  37797  bj-sblem1  37846  bj-sblem2  37847  bj-ceqsalt0  37888  bj-ceqsalt1  37889  bj-axseprep  38082  wl-spae  38546  wl-aetr  38554  wl-axc11r  38555  wl-aleq  38560  wl-nfeqfb  38561  axc11-o  40101  pm10.57  45448  2al2imi  45450  19.41rg  45626  hbntal  45629  quantgodelALT  47978