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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057

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-ex 1781  df-rex 3058

This theorem is referenced by:  reximdvai  3144  reximssdv  3151  ssrexvOLD  4004  ssimaex  6913  nnsuc  7820  oaass  8482  omeulem1  8503  ssnnfi  9086  findcard3  9174  unfilem1  9196  epfrs  9628  alephval3  10008  isfin7-2  10294  fpwwe2lem12  10540  inawinalem  10587  ico0  13293  ioc0  13294  r19.2uz  15261  climrlim2  15456  prmdvdsncoprmbd  16640  iserodd  16749  ramub2  16928  prmgaplem6  16970  ghmqusnsglem2  19195  ghmquskerlem2  19199  ablfaclem3  20003  unitgrp  20303  restnlly  23398  llyrest  23401  nllyrest  23402  llyidm  23404  nllyidm  23405  cnpflfi  23915  cnextcn  23983  ivthlem3  25382  dvfsumrlim  25966  lgsquadlem2  27320  oppperpex  28732  outpasch  28734  ushgredgedg  29209  ushgredgedgloop  29211  cusgrfilem2  29437  nsgqusf1olem2  33386  ssmxidl  33446  cmppcmp  33892  eulerpartlemgvv  34410  eulerpartlemgh  34412  fnrelpredd  35123  r1filimi  35135  erdszelem7  35262  rellysconn  35316  ivthALT  36400  fnessref  36422  phpreu  37664  poimirlem26  37706  itg2gt0cn  37735  frinfm  37795  sstotbnd2  37834  heiborlem3  37873  isdrngo3  38019  dihjat1lem  41547  dvh1dim  41561  dochsatshp  41570  mapdpglem2  41792  prjspreln0  42727  pellexlem5  42950  pell14qrss1234  42973  pell1qrss14  42985  lnr2i  43233  hbtlem6  43246  dflim5  43446  tfsconcatrn  43459  naddgeoa  43511  mnuop3d  44388  fvelsetpreimafv  47511  opnneir  49031