Theorem al2imi 1783

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

Syntax hints:   → wi 4  ∀wal 1521

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

This theorem is referenced by:  alanimi  1784  alimdh  1785  albi  1786  aleximi  1799  19.33b  1853  aevlem0  2022  axc16g  2172  axc11rvOLD  2178  axc11r  2223  axc10  2288  sbequi  2403  sbi1  2420  moim  2548  2eu6  2587  ral2imi  2976  ceqsalt  3259  difin0ss  3979  hbntg  31835  bj-2alim  32719  bj-ssbim  32746  bj-axc10v  32842  bj-ceqsalt0  32998  bj-ceqsalt1  32999  wl-spae  33436  wl-aetr  33447  wl-aleq  33452  wl-nfeqfb  33453  axc11-o  34555  pm10.57  38887  2al2imi  38889  19.41rg  39083  hbntal  39086