Theorem ral2imi 3079

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

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  ∀wral 3054

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

This theorem depends on definitions:  df-bi 208  df-ral 3055

This theorem is referenced by:  ralim  3080  rexim  3081  ralbi  3095  r19.26  3100  falseral0  4449  replem  5217  iiner  8733  ss2ixp  8855  undifixp  8879  boxriin  8885  acni2  9966  axcc4  10359  intgru  10735  ingru  10736  prdsdsval3  17446  mndind  18794  hauscmplem  23396  uspgr2wlkeq  29739  wlkp1lem8  29772  prdstotbnd  38168  mnuunid  44728