Theorem ralimdv2 2990

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

Hypothesis

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

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem ralimdv2

Step	Hyp	Ref	Expression
1		ralimdv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒)))
2	1	alimdv 1885	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)))
3		df-ral 2946	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 2946	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))
5	2, 3, 4	3imtr4g 285	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4  ∀wal 1521   ∈ wcel 2030  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-ral 2946

This theorem is referenced by:  ralimdva  2991  ssralv  3699  zorn2lem7  9362  pwfseqlem3  9520  sup2  11017  xrsupexmnf  12173  xrinfmexpnf  12174  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  r19.29uz  14134  rexuzre  14136  caurcvg  14451  caucvg  14453  isprm5  15466  prmgaplem5  15806  prmgaplem6  15807  mrissmrid  16348  elcls3  20935  iscnp4  21115  cncls2  21125  cnntr  21127  2ndcsep  21310  dyadmbllem  23413  xrlimcnp  24740  pntlem3  25343  sigaclfu2  30312  mapdordlem2  37243  iunrelexp0  38311  climrec  40153  0ellimcdiv  40199