Theorem ral2imi 3124

Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3130. (Revised by Wolf Lammen, 1-Dec-2019.)

Hypothesis

Ref	Expression
ral2imi.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ral2imi	⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Proof of Theorem ral2imi

Step	Hyp	Ref	Expression
1		df-ral 3111	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		ral2imi.1	. . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imim3i 64	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	al2imi 1817	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)))
5		df-ral 3111	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
6		df-ral 3111	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))
7	4, 5, 6	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
8	1, 7	sylbi 220	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4  ∀wal 1536   ∈ wcel 2111  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 210  df-ral 3111

This theorem is referenced by:  ralim  3130  ralbi  3135  r19.26  3137  rexim  3204  iiner  8352  ss2ixp  8457  undifixp  8481  boxriin  8487  acni2  9457  axcc4  9850  intgru  10225  ingru  10226  prdsdsval3  16750  mndind  17984  hauscmplem  22011  uspgr2wlkeq  27435  wlkp1lem8  27470  prdstotbnd  35232  mnuunid  40985