Theorem ral2imi 3102

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  ralim  3103  rexim  3104  ralbi  3118  r19.26  3123  falseral0  4470  replem  5241  iiner  8803  ss2ixp  8931  undifixp  8955  boxriin  8961  acni2  10118  axcc4  10510  intgru  10892  ingru  10893  prdsdsval3  17649  mndind  19017  hauscmplem  23717  uspgr2wlkeq  30219  wlkp1lem8  30252  prdstotbnd  38708  mnuunid  45246