Theorem reximdv2 3142

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  reximdvai  3143  reximssdv  3150  ssrexvOLD  4008  ssimaex  6907  nnsuc  7814  oaass  8476  omeulem1  8497  ssnnfi  9079  findcard3  9167  unfilem1  9189  epfrs  9621  alephval3  9998  isfin7-2  10284  fpwwe2lem12  10530  inawinalem  10577  ico0  13288  ioc0  13289  r19.2uz  15256  climrlim2  15451  prmdvdsncoprmbd  16635  iserodd  16744  ramub2  16923  prmgaplem6  16965  ghmqusnsglem2  19191  ghmquskerlem2  19195  ablfaclem3  19999  unitgrp  20299  restnlly  23395  llyrest  23398  nllyrest  23399  llyidm  23401  nllyidm  23402  cnpflfi  23912  cnextcn  23980  ivthlem3  25379  dvfsumrlim  25963  lgsquadlem2  27317  oppperpex  28729  outpasch  28731  ushgredgedg  29205  ushgredgedgloop  29207  cusgrfilem2  29433  nsgqusf1olem2  33374  ssmxidl  33434  cmppcmp  33866  eulerpartlemgvv  34384  eulerpartlemgh  34386  fnrelpredd  35097  r1filimi  35106  erdszelem7  35229  rellysconn  35283  ivthALT  36368  fnessref  36390  phpreu  37643  poimirlem26  37685  itg2gt0cn  37714  frinfm  37774  sstotbnd2  37813  heiborlem3  37852  isdrngo3  37998  dihjat1lem  41466  dvh1dim  41480  dochsatshp  41489  mapdpglem2  41711  prjspreln0  42641  pellexlem5  42865  pell14qrss1234  42888  pell1qrss14  42900  lnr2i  43148  hbtlem6  43161  dflim5  43361  tfsconcatrn  43374  naddgeoa  43426  mnuop3d  44303  fvelsetpreimafv  47417  opnneir  48937