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 1540

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  1835  19.33b  1889  aevlem0  2058  sbi1  2075  axc16g  2252  axc11r  2366  axc10  2385  axc15  2422  sb2  2479  moim  2539  2eu6  2653  ral2imi  3086  ceqsalt  3506  elabgt  3663  difin0ss  4369  axprlem2  5423  hbntg  34777  bj-2alim  35488  bj-cbvalimt  35516  bj-axc10v  35671  bj-sblem1  35721  bj-sblem2  35722  bj-ceqsalt0  35764  bj-ceqsalt1  35765  wl-spae  36390  wl-aetr  36398  wl-axc11r  36399  wl-aleq  36404  wl-nfeqfb  36405  axc11-o  37821  pm10.57  43130  2al2imi  43132  19.41rg  43311  hbntal  43314