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 1536

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  1833  19.33b  1886  aevlem0  2059  sbi1  2076  axc16g  2258  sbi1vOLD  2317  axc11r  2375  axc10  2392  axc15  2433  sb2  2493  sbi1OLD  2519  sbequiALT  2572  sbi1ALT  2582  moim  2602  2eu6  2719  ral2imi  3124  ceqsalt  3474  difin0ss  4282  axprlem2  5290  hbntg  33163  bj-2alim  34057  bj-cbvalimt  34085  bj-axc10v  34230  bj-sblem1  34281  bj-sblem2  34282  bj-ceqsalt0  34324  bj-ceqsalt1  34325  wl-spae  34926  wl-aetr  34934  wl-axc11r  34935  wl-aleq  34940  wl-nfeqfb  34941  axc11-o  36247  pm10.57  41075  2al2imi  41077  19.41rg  41256  hbntal  41259