Theorem al2imi 1809

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

Syntax hints:   → wi 4  ∀wal 1531

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

This theorem is referenced by:  alanimi  1810  alimdh  1811  albi  1812  aleximi  1826  19.33b  1880  aevlem0  2049  sbi1  2066  axc16g  2246  axc11r  2359  axc10  2378  axc15  2415  sb2  2472  moim  2532  2eu6  2645  ral2imi  3075  ceqsalt  3496  elabgt  3658  elabgtOLD  3659  sstr2  3984  ssralv  4046  difin0ss  4369  axprlem2  5423  hbntg  35471  bj-2alim  36157  bj-cbvalimt  36185  bj-axc10v  36340  bj-sblem1  36389  bj-sblem2  36390  bj-ceqsalt0  36432  bj-ceqsalt1  36433  wl-spae  37058  wl-aetr  37066  wl-axc11r  37067  wl-aleq  37072  wl-nfeqfb  37073  axc11-o  38492  pm10.57  43873  2al2imi  43875  19.41rg  44054  hbntal  44057