Theorem al2imi 1810

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

Syntax hints:   → wi 4  ∀wal 1532

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

This theorem is referenced by:  alanimi  1811  alimdh  1812  albi  1813  aleximi  1827  19.33b  1881  aevlem0  2050  sbi1  2067  axc16g  2244  axc11r  2360  axc10  2379  axc15  2416  sb2  2473  moim  2533  2eu6  2647  ral2imi  3080  ceqsalt  3501  elabgt  3658  elabgtOLD  3659  difin0ss  4364  axprlem2  5418  hbntg  35337  bj-2alim  36023  bj-cbvalimt  36051  bj-axc10v  36206  bj-sblem1  36255  bj-sblem2  36256  bj-ceqsalt0  36298  bj-ceqsalt1  36299  wl-spae  36924  wl-aetr  36932  wl-axc11r  36933  wl-aleq  36938  wl-nfeqfb  36939  axc11-o  38360  pm10.57  43731  2al2imi  43733  19.41rg  43912  hbntal  43915