Theorem al2imi 1819

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  alanimi  1820  alimdh  1821  albi  1822  aleximi  1835  19.33b  1889  aevlem0  2058  sbi1  2075  axc16g  2255  axc11r  2366  axc10  2385  axc15  2422  sb2  2480  moim  2544  2eu6  2658  ral2imi  3081  ceqsalt  3452  elabgt  3596  difin0ss  4299  axprlem2  5342  hbntg  33687  bj-2alim  34719  bj-cbvalimt  34747  bj-axc10v  34902  bj-sblem1  34953  bj-sblem2  34954  bj-ceqsalt0  34996  bj-ceqsalt1  34997  wl-spae  35607  wl-aetr  35615  wl-axc11r  35616  wl-aleq  35621  wl-nfeqfb  35622  axc11-o  36892  pm10.57  41878  2al2imi  41880  19.41rg  42059  hbntal  42062