Theorem al2imi 1809

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

Syntax hints:   → wi 4  ∀wal 1531

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

This theorem is referenced by:  alanimi  1810  alimdh  1811  albi  1812  aleximi  1826  19.33b  1880  aevlem0  2049  sbi1  2066  axc16g  2246  axc11r  2359  axc10  2378  axc15  2415  sb2  2472  moim  2532  2eu6  2645  ral2imi  3074  ceqsalt  3494  elabgt  3657  elabgtOLD  3658  sstr2  3983  ssralv  4045  difin0ss  4370  axprlem2  5424  hbntg  35529  bj-2alim  36215  bj-cbvalimt  36243  bj-axc10v  36398  bj-sblem1  36447  bj-sblem2  36448  bj-ceqsalt0  36490  bj-ceqsalt1  36491  wl-spae  37116  wl-aetr  37124  wl-axc11r  37125  wl-aleq  37130  wl-nfeqfb  37131  axc11-o  38550  pm10.57  43947  2al2imi  43949  19.41rg  44128  hbntal  44131