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 1531

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  1828  19.33b  1882  aevlem0  2055  sbi1  2072  axc16g  2257  sbi1vOLD  2319  axc11r  2382  axc10  2399  axc15  2440  sb2  2500  sbequiOLD  2530  sbi1OLD  2538  sbequiALT  2592  sbi1ALT  2602  moim  2622  2eu6  2740  ral2imi  3156  ceqsalt  3527  difin0ss  4327  axprlem2  5316  hbntg  33045  bj-2alim  33939  bj-cbvalimt  33967  bj-axc10v  34110  bj-sblem1  34161  bj-sblem2  34162  bj-ceqsalt0  34195  bj-ceqsalt1  34196  wl-spae  34755  wl-aetr  34763  wl-axc11r  34764  wl-aleq  34769  wl-nfeqfb  34770  axc11-o  36081  pm10.57  40696  2al2imi  40698  19.41rg  40877  hbntal  40880