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  3461  elabgt  3604  difin0ss  4304  axprlem2  5347  hbntg  33768  bj-2alim  34779  bj-cbvalimt  34807  bj-axc10v  34962  bj-sblem1  35013  bj-sblem2  35014  bj-ceqsalt0  35056  bj-ceqsalt1  35057  wl-spae  35667  wl-aetr  35675  wl-axc11r  35676  wl-aleq  35681  wl-nfeqfb  35682  axc11-o  36952  pm10.57  41949  2al2imi  41951  19.41rg  42130  hbntal  42133