Theorem ralimdv2 3147

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 1918	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)))
3		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))
5	2, 3, 4	3imtr4g 296	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  ax-5 1912

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

This theorem is referenced by:  ralimdva  3150  ssralvOLD  3995  zorn2lem7  10418  pwfseqlem3  10577  sup2  12106  xrsupexmnf  13251  xrinfmexpnf  13252  xrsupsslem  13253  xrinfmsslem  13254  xrub  13258  r19.29uz  15307  rexuzre  15309  caurcvg  15633  caucvg  15635  isprm5  16671  prmgaplem5  17020  prmgaplem6  17021  mrissmrid  17601  elcls3  23061  iscnp4  23241  cncls2  23251  cnntr  23253  2ndcsep  23437  dyadmbllem  25579  xrlimcnp  26948  pntlem3  27589  fldextrspunlsplem  33836  sigaclfu2  34284  lfuhgr2  35320  rdgssun  37711  mapdordlem2  42100  aks6d1c1  42572  sn-sup2  42953  dffltz  43084  cantnfresb  43773  safesnsupfiub  43864  iunrelexp0  44150  climrec  46054  0ellimcdiv  46098  pgindnf  50206