Theorem reximdv2 3164

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070

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 3071

This theorem is referenced by:  reximdvai  3165  reximssdv  3173  ssrexvOLD  4057  ssimaex  6994  nnsuc  7905  oaass  8599  omeulem1  8620  ssnnfi  9209  findcard3  9318  findcard3OLD  9319  unfilem1  9343  epfrs  9771  alephval3  10150  isfin7-2  10436  fpwwe2lem12  10682  inawinalem  10729  ico0  13433  ioc0  13434  r19.2uz  15390  climrlim2  15583  prmdvdsncoprmbd  16764  iserodd  16873  ramub2  17052  prmgaplem6  17094  ghmqusnsglem2  19299  ghmquskerlem2  19303  ablfaclem3  20107  unitgrp  20383  restnlly  23490  llyrest  23493  nllyrest  23494  llyidm  23496  nllyidm  23497  cnpflfi  24007  cnextcn  24075  ivthlem3  25488  dvfsumrlim  26072  lgsquadlem2  27425  oppperpex  28761  outpasch  28763  ushgredgedg  29246  ushgredgedgloop  29248  cusgrfilem2  29474  nsgqusf1olem2  33442  ssmxidl  33502  cmppcmp  33857  eulerpartlemgvv  34378  eulerpartlemgh  34380  fnrelpredd  35103  erdszelem7  35202  rellysconn  35256  ivthALT  36336  fnessref  36358  phpreu  37611  poimirlem26  37653  itg2gt0cn  37682  frinfm  37742  sstotbnd2  37781  heiborlem3  37820  isdrngo3  37966  dihjat1lem  41430  dvh1dim  41444  dochsatshp  41453  mapdpglem2  41675  prjspreln0  42619  pellexlem5  42844  pell14qrss1234  42867  pell1qrss14  42879  lnr2i  43128  hbtlem6  43141  dflim5  43342  tfsconcatrn  43355  naddgeoa  43407  mnuop3d  44290  fvelsetpreimafv  47374  opnneir  48804