Theorem ralimdv2 3145

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ralimdva  3148  ssralvOLD  4006  zorn2lem7  10412  pwfseqlem3  10571  sup2  12098  xrsupexmnf  13220  xrinfmexpnf  13221  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  r19.29uz  15274  rexuzre  15276  caurcvg  15600  caucvg  15602  isprm5  16634  prmgaplem5  16983  prmgaplem6  16984  mrissmrid  17564  elcls3  23027  iscnp4  23207  cncls2  23217  cnntr  23219  2ndcsep  23403  dyadmbllem  25556  xrlimcnp  26934  pntlem3  27576  fldextrspunlsplem  33830  sigaclfu2  34278  lfuhgr2  35313  rdgssun  37583  mapdordlem2  41897  aks6d1c1  42370  sn-sup2  42746  dffltz  42877  cantnfresb  43566  safesnsupfiub  43657  iunrelexp0  43943  climrec  45849  0ellimcdiv  45893  pgindnf  49961