Theorem al2imi 1818

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  alanimi  1819  alimdh  1820  albi  1821  aleximi  1834  19.33b  1888  aevlem0  2057  sbi1  2074  axc16g  2252  axc11r  2366  axc10  2385  axc15  2422  sb2  2480  moim  2544  2eu6  2658  ral2imi  3082  ceqsalt  3462  elabgt  3603  difin0ss  4302  axprlem2  5347  hbntg  33781  bj-2alim  34792  bj-cbvalimt  34820  bj-axc10v  34975  bj-sblem1  35026  bj-sblem2  35027  bj-ceqsalt0  35069  bj-ceqsalt1  35070  wl-spae  35680  wl-aetr  35688  wl-axc11r  35689  wl-aleq  35694  wl-nfeqfb  35695  axc11-o  36965  pm10.57  41989  2al2imi  41991  19.41rg  42170  hbntal  42173