Theorem al2imi 1834

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

Syntax hints:   → wi 4  ∀wal 1557

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

This theorem is referenced by:  alanimi  1835  alimdh  1836  albi  1837  aleximi  1851  19.33b  1904  aevlem0  2075  sbi1lem  2101  sbi1ALT  2103  axc16g  2294  axc11r  2398  axc10  2415  axc15  2452  sb2  2509  moim  2570  2eu6  2682  ral2imi  3100  ceqsalt  3486  spcimgft  3513  elabgtOLD  3632  sstr2  3943  ssralv  4005  difin0ss  4325  sepexlem  5248  axprlem2  5380  axprglem  5392  axsepg2  35400  axsepg4  35403  axnulg  35405  axpowg2  35407  axpowg3  35408  hbntg  36117  axtco2  36798  axnulregtco  36804  bj-alsyl  37028  bj-2alim  37029  bj-alimdh  37030  bj-hbald  37118  bj-axc10v  37242  bj-sblem1  37291  bj-sblem2  37292  bj-ceqsalt0  37333  bj-ceqsalt1  37334  bj-axseprep  37523  wl-spae  37988  wl-aetr  37996  wl-axc11r  37997  wl-aleq  38002  wl-nfeqfb  38003  axc11-o  39539  pm10.57  44911  2al2imi  44913  19.41rg  45090  hbntal  45093  quantgodelALT  47413