Theorem ralimi2 3084

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 1809	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
3		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
5	2, 3, 4	3imtr4i 292	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108  ∀wral 3067

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

This theorem depends on definitions:  df-bi 207  df-ral 3068

This theorem is referenced by:  ralimia  3086  ralcom3OLD  3104  tfi  7890  resixpfo  8994  omex  9712  kmlem1  10220  brdom5  10598  brdom4  10599  xrub  13374  pcmptcl  16938  itgeq2  25833  iblcnlem  25844  pntrsumbnd  27628  nmounbseqi  30809  nmounbseqiALT  30810  sumdmdi  32452  dmdbr4ati  32453  dmdbr6ati  32455  bnj110  34834  fiinfi  43535