Theorem al2imi 1816

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

Syntax hints:   → wi 4  ∀wal 1539

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

This theorem is referenced by:  alanimi  1817  alimdh  1818  albi  1819  aleximi  1833  19.33b  1886  aevlem0  2057  sbi1  2076  axc16g  2265  axc11r  2370  axc10  2387  axc15  2424  sb2  2481  moim  2541  2eu6  2654  ral2imi  3072  ceqsalt  3471  spcimgft  3500  elabgtOLD  3624  elabgtOLDOLD  3625  sstr2  3937  ssralv  3999  difin0ss  4322  sepexlem  5239  axprlem2  5364  axnulg  35140  hbntg  35868  bj-2alim  36675  bj-cbvalimt  36704  bj-axc10v  36858  bj-sblem1  36907  bj-sblem2  36908  bj-ceqsalt0  36949  bj-ceqsalt1  36950  wl-spae  37586  wl-aetr  37594  wl-axc11r  37595  wl-aleq  37600  wl-nfeqfb  37601  axc11-o  39070  pm10.57  44488  2al2imi  44490  19.41rg  44667  hbntal  44670