Theorem reximdv2 3147

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 1919	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3062	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3062	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 296	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

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-ex 1782  df-rex 3062

This theorem is referenced by:  reximdvai  3148  reximssdv  3155  ssrexvOLD  3995  ssimaex  6925  nnsuc  7835  oaass  8496  omeulem1  8517  ssnnfi  9104  findcard3  9193  unfilem1  9215  epfrs  9652  alephval3  10032  isfin7-2  10318  fpwwe2lem12  10565  inawinalem  10612  ico0  13344  ioc0  13345  r19.2uz  15314  climrlim2  15509  prmdvdsncoprmbd  16697  iserodd  16806  ramub2  16985  prmgaplem6  17027  ghmqusnsglem2  19256  ghmquskerlem2  19260  ablfaclem3  20064  unitgrp  20363  restnlly  23447  llyrest  23450  nllyrest  23451  llyidm  23453  nllyidm  23454  cnpflfi  23964  cnextcn  24032  ivthlem3  25420  dvfsumrlim  25998  lgsquadlem2  27344  oppperpex  28821  outpasch  28823  ushgredgedg  29298  ushgredgedgloop  29300  cusgrfilem2  29525  nsgqusf1olem2  33474  ssmxidl  33534  cmppcmp  34002  eulerpartlemgvv  34520  eulerpartlemgh  34522  fnrelpredd  35234  r1filimi  35246  noinfepfnregs  35276  erdszelem7  35379  rellysconn  35433  ivthALT  36517  fnessref  36539  phpreu  37925  poimirlem26  37967  itg2gt0cn  37996  frinfm  38056  sstotbnd2  38095  heiborlem3  38134  isdrngo3  38280  dihjat1lem  41874  dvh1dim  41888  dochsatshp  41897  mapdpglem2  42119  prjspreln0  43042  pellexlem5  43261  pell14qrss1234  43284  pell1qrss14  43296  lnr2i  43544  hbtlem6  43557  dflim5  43757  tfsconcatrn  43770  naddgeoa  43822  mnuop3d  44698  fvelsetpreimafv  47847  opnneir  49382