Theorem al2imi 1815

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  alanimi  1816  alimdh  1817  albi  1818  aleximi  1832  19.33b  1886  aevlem0  2055  sbi1  2072  axc16g  2249  axc11r  2363  axc10  2382  axc15  2419  sb2  2476  moim  2536  2eu6  2650  ral2imi  3083  ceqsalt  3504  elabgt  3661  difin0ss  4367  axprlem2  5421  hbntg  35081  bj-2alim  35791  bj-cbvalimt  35819  bj-axc10v  35974  bj-sblem1  36024  bj-sblem2  36025  bj-ceqsalt0  36067  bj-ceqsalt1  36068  wl-spae  36693  wl-aetr  36701  wl-axc11r  36702  wl-aleq  36707  wl-nfeqfb  36708  axc11-o  38124  pm10.57  43432  2al2imi  43434  19.41rg  43613  hbntal  43616