Theorem reximdv2 3198

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-rex 3069

This theorem is referenced by:  reximdvai  3199  reximssdv  3204  ssrexv  3984  ssimaex  6835  nnsuc  7705  oaass  8354  omeulem1  8375  ssnnfi  8914  ssnnfiOLD  8915  findcard3  8987  unfilem1  9008  trpredrec  9415  epfrs  9420  alephval3  9797  isfin7-2  10083  fpwwe2lem12  10329  inawinalem  10376  ico0  13054  ioc0  13055  r19.2uz  14991  climrlim2  15184  prmdvdsncoprmbd  16359  iserodd  16464  ramub2  16643  prmgaplem6  16685  ablfaclem3  19605  unitgrp  19824  restnlly  22541  llyrest  22544  nllyrest  22545  llyidm  22547  nllyidm  22548  cnpflfi  23058  cnextcn  23126  ivthlem3  24522  dvfsumrlim  25100  lgsquadlem2  26434  oppperpex  27018  outpasch  27020  ushgredgedg  27499  ushgredgedgloop  27501  cusgrfilem2  27726  nsgqusf1olem2  31501  ssmxidl  31544  cmppcmp  31710  eulerpartlemgvv  32243  eulerpartlemgh  32245  fnrelpredd  32961  erdszelem7  33059  rellysconn  33113  ivthALT  34451  fnessref  34473  phpreu  35688  poimirlem26  35730  itg2gt0cn  35759  frinfm  35820  sstotbnd2  35859  heiborlem3  35898  isdrngo3  36044  dihjat1lem  39369  dvh1dim  39383  dochsatshp  39392  mapdpglem2  39614  prjspreln0  40369  pellexlem5  40571  pell14qrss1234  40594  pell1qrss14  40606  lnr2i  40857  hbtlem6  40870  mnuop3d  41778  fvelsetpreimafv  44727  opnneir  46088