Theorem al2imi 1814

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  alanimi  1815  alimdh  1816  albi  1817  aleximi  1831  19.33b  1884  aevlem0  2053  sbi1  2070  axc16g  2259  axc11r  2370  axc10  2389  axc15  2426  sb2  2483  moim  2543  2eu6  2656  ral2imi  3084  ceqsalt  3514  spcimgft  3545  elabgt  3671  elabgtOLD  3672  sstr2  3989  ssralv  4051  difin0ss  4372  sepexlem  5298  axprlem2  5423  axnulg  35107  hbntg  35807  bj-2alim  36612  bj-cbvalimt  36641  bj-axc10v  36795  bj-sblem1  36844  bj-sblem2  36845  bj-ceqsalt0  36886  bj-ceqsalt1  36887  wl-spae  37523  wl-aetr  37531  wl-axc11r  37532  wl-aleq  37537  wl-nfeqfb  37538  axc11-o  38953  pm10.57  44395  2al2imi  44397  19.41rg  44575  hbntal  44578