Theorem al2imi 1812

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

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  alanimi  1813  alimdh  1814  albi  1815  aleximi  1829  19.33b  1883  aevlem0  2052  sbi1  2069  axc16g  2258  axc11r  2369  axc10  2388  axc15  2425  sb2  2482  moim  2542  2eu6  2655  ral2imi  3083  ceqsalt  3513  spcimgft  3546  elabgt  3672  elabgtOLD  3673  sstr2  4002  ssralv  4064  difin0ss  4379  sepexlem  5305  axprlem2  5430  axnulg  35085  hbntg  35787  bj-2alim  36593  bj-cbvalimt  36622  bj-axc10v  36776  bj-sblem1  36825  bj-sblem2  36826  bj-ceqsalt0  36867  bj-ceqsalt1  36868  wl-spae  37502  wl-aetr  37510  wl-axc11r  37511  wl-aleq  37516  wl-nfeqfb  37517  axc11-o  38933  pm10.57  44367  2al2imi  44369  19.41rg  44548  hbntal  44551