Theorem reximdv2 3143

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)

Hypothesis

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

Assertion

Ref	Expression
reximdv2	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reximdv2

Step	Hyp	Ref	Expression
1		reximdv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))
2	1	eximdv 1917	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3054	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3054	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 296	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3054

This theorem is referenced by:  reximdvai  3144  reximssdv  3151  ssrexvOLD  4020  ssimaex  6946  nnsuc  7860  oaass  8525  omeulem1  8546  ssnnfi  9133  findcard3  9229  findcard3OLD  9230  unfilem1  9254  epfrs  9684  alephval3  10063  isfin7-2  10349  fpwwe2lem12  10595  inawinalem  10642  ico0  13352  ioc0  13353  r19.2uz  15318  climrlim2  15513  prmdvdsncoprmbd  16697  iserodd  16806  ramub2  16985  prmgaplem6  17027  ghmqusnsglem2  19213  ghmquskerlem2  19217  ablfaclem3  20019  unitgrp  20292  restnlly  23369  llyrest  23372  nllyrest  23373  llyidm  23375  nllyidm  23376  cnpflfi  23886  cnextcn  23954  ivthlem3  25354  dvfsumrlim  25938  lgsquadlem2  27292  oppperpex  28680  outpasch  28682  ushgredgedg  29156  ushgredgedgloop  29158  cusgrfilem2  29384  nsgqusf1olem2  33385  ssmxidl  33445  cmppcmp  33848  eulerpartlemgvv  34367  eulerpartlemgh  34369  fnrelpredd  35079  erdszelem7  35184  rellysconn  35238  ivthALT  36323  fnessref  36345  phpreu  37598  poimirlem26  37640  itg2gt0cn  37669  frinfm  37729  sstotbnd2  37768  heiborlem3  37807  isdrngo3  37953  dihjat1lem  41422  dvh1dim  41436  dochsatshp  41445  mapdpglem2  41667  prjspreln0  42597  pellexlem5  42821  pell14qrss1234  42844  pell1qrss14  42856  lnr2i  43105  hbtlem6  43118  dflim5  43318  tfsconcatrn  43331  naddgeoa  43383  mnuop3d  44260  fvelsetpreimafv  47388  opnneir  48895