Theorem ralimi2 3085

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)

Hypothesis

Ref	Expression
ralimi2.1	⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓))

Assertion

Ref	Expression
ralimi2	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

Proof of Theorem ralimi2

Step	Hyp	Ref	Expression
1		ralimi2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓))
2	1	alimi 1817	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
3		df-ral 3070	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3070	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
5	2, 3, 4	3imtr4i 291	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2109  ∀wral 3065

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

This theorem depends on definitions:  df-bi 206  df-ral 3070

This theorem is referenced by:  ralimia  3086  ralcom3  3291  tfi  7688  resixpfo  8698  omex  9362  kmlem1  9890  brdom5  10269  brdom4  10270  xrub  13028  pcmptcl  16573  itgeq2  24923  iblcnlem  24934  pntrsumbnd  26695  nmounbseqi  29118  nmounbseqiALT  29119  sumdmdi  30761  dmdbr4ati  30762  dmdbr6ati  30764  bnj110  32817  fiinfi  41133