Theorem al2imi 1900

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

Syntax hints:   → wi 4  ∀wal 1635

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

This theorem is referenced by:  alanimi  1901  alimdh  1902  albi  1903  aleximi  1916  19.33b  1975  aevlem0  2149  axc16g  2313  axc11rvOLD  2319  axc11r  2363  axc10  2428  sbequi  2536  sbi1  2553  moim  2693  2eu6  2733  ral2imi  3146  ceqsalt  3433  difin0ss  4158  hbntg  32052  bj-2alim  32930  bj-ssbim  32958  bj-axc10v  33053  bj-ceqsalt0  33199  bj-ceqsalt1  33200  wl-spae  33640  wl-aetr  33649  wl-aleq  33654  wl-nfeqfb  33655  axc11-o  34748  pm10.57  39087  2al2imi  39089  19.41rg  39281  hbntal  39284