Theorem ral2imi 3077

Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3078. (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 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		ral2imi.1	. . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imim3i 64	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	al2imi 1817	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)))
5		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
6		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))
7	4, 5, 6	3imtr4g 296	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
8	1, 7	sylbi 217	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

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 207  df-ral 3053

This theorem is referenced by:  ralim  3078  rexim  3079  ralbi  3093  r19.26  3098  falseral0  4455  replem  5223  iiner  8729  ss2ixp  8851  undifixp  8875  boxriin  8881  acni2  9959  axcc4  10352  intgru  10728  ingru  10729  prdsdsval3  17439  mndind  18787  hauscmplem  23381  uspgr2wlkeq  29729  wlkp1lem8  29762  prdstotbnd  38129  mnuunid  44722