Theorem reximdv2 3161

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1775   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-rex 3068

This theorem is referenced by:  reximdvai  3162  reximssdv  3170  ssrexvOLD  4068  ssimaex  6993  nnsuc  7904  oaass  8597  omeulem1  8618  ssnnfi  9207  findcard3  9315  findcard3OLD  9316  unfilem1  9340  epfrs  9768  alephval3  10147  isfin7-2  10433  fpwwe2lem12  10679  inawinalem  10726  ico0  13429  ioc0  13430  r19.2uz  15386  climrlim2  15579  prmdvdsncoprmbd  16760  iserodd  16868  ramub2  17047  prmgaplem6  17089  ghmqusnsglem2  19311  ghmquskerlem2  19315  ablfaclem3  20121  unitgrp  20399  restnlly  23505  llyrest  23508  nllyrest  23509  llyidm  23511  nllyidm  23512  cnpflfi  24022  cnextcn  24090  ivthlem3  25501  dvfsumrlim  26086  lgsquadlem2  27439  oppperpex  28775  outpasch  28777  ushgredgedg  29260  ushgredgedgloop  29262  cusgrfilem2  29488  nsgqusf1olem2  33421  ssmxidl  33481  cmppcmp  33818  eulerpartlemgvv  34357  eulerpartlemgh  34359  fnrelpredd  35081  erdszelem7  35181  rellysconn  35235  ivthALT  36317  fnessref  36339  phpreu  37590  poimirlem26  37632  itg2gt0cn  37661  frinfm  37721  sstotbnd2  37760  heiborlem3  37799  isdrngo3  37945  dihjat1lem  41410  dvh1dim  41424  dochsatshp  41433  mapdpglem2  41655  prjspreln0  42595  pellexlem5  42820  pell14qrss1234  42843  pell1qrss14  42855  lnr2i  43104  hbtlem6  43117  dflim5  43318  tfsconcatrn  43331  naddgeoa  43383  mnuop3d  44266  fvelsetpreimafv  47311  opnneir  48702