Theorem al2imi 1817

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  alanimi  1818  alimdh  1819  albi  1820  aleximi  1834  19.33b  1887  aevlem0  2058  sbi1  2077  axc16g  2268  axc11r  2373  axc10  2390  axc15  2427  sb2  2484  moim  2545  2eu6  2658  ral2imi  3077  ceqsalt  3464  spcimgft  3492  elabgtOLD  3616  elabgtOLDOLD  3617  sstr2  3929  ssralv  3991  difin0ss  4314  sepexlem  5234  axprlem2  5361  axprglem  5373  axnulg  35267  hbntg  36001  axtco2  36672  axnulregtco  36678  bj-alsyl  36902  bj-2alim  36903  bj-alimdh  36904  bj-hbald  36992  bj-axc10v  37116  bj-sblem1  37165  bj-sblem2  37166  bj-ceqsalt0  37207  bj-ceqsalt1  37208  bj-axseprep  37397  wl-spae  37860  wl-aetr  37868  wl-axc11r  37869  wl-aleq  37874  wl-nfeqfb  37875  axc11-o  39411  pm10.57  44816  2al2imi  44818  19.41rg  44995  hbntal  44998