Theorem ralimi2 3070

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 1813	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
3		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
5	2, 3, 4	3imtr4i 292	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:  ralimia  3072  tfi  7798  resixpfo  8878  omex  9558  kmlem1  10067  brdom5  10445  brdom4  10446  xrub  13258  pcmptcl  16856  itgeq2  25758  iblcnlem  25769  pntrsumbnd  27546  nmounbseqi  30866  nmounbseqiALT  30867  sumdmdi  32509  dmdbr4ati  32510  dmdbr6ati  32512  bnj110  35019  fiinfi  44021