Theorem reximdv2 3148

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3063

This theorem is referenced by:  reximdvai  3149  reximssdv  3156  ssrexvOLD  4009  ssimaex  6927  nnsuc  7836  oaass  8498  omeulem1  8519  ssnnfi  9106  findcard3  9195  unfilem1  9217  epfrs  9652  alephval3  10032  isfin7-2  10318  fpwwe2lem12  10565  inawinalem  10612  ico0  13319  ioc0  13320  r19.2uz  15287  climrlim2  15482  prmdvdsncoprmbd  16666  iserodd  16775  ramub2  16954  prmgaplem6  16996  ghmqusnsglem2  19222  ghmquskerlem2  19226  ablfaclem3  20030  unitgrp  20331  restnlly  23438  llyrest  23441  nllyrest  23442  llyidm  23444  nllyidm  23445  cnpflfi  23955  cnextcn  24023  ivthlem3  25422  dvfsumrlim  26006  lgsquadlem2  27360  oppperpex  28837  outpasch  28839  ushgredgedg  29314  ushgredgedgloop  29316  cusgrfilem2  29542  nsgqusf1olem2  33506  ssmxidl  33566  cmppcmp  34035  eulerpartlemgvv  34553  eulerpartlemgh  34555  fnrelpredd  35266  r1filimi  35278  noinfepfnregs  35307  erdszelem7  35410  rellysconn  35464  ivthALT  36548  fnessref  36570  phpreu  37849  poimirlem26  37891  itg2gt0cn  37920  frinfm  37980  sstotbnd2  38019  heiborlem3  38058  isdrngo3  38204  dihjat1lem  41798  dvh1dim  41812  dochsatshp  41821  mapdpglem2  42043  prjspreln0  42961  pellexlem5  43184  pell14qrss1234  43207  pell1qrss14  43219  lnr2i  43467  hbtlem6  43480  dflim5  43680  tfsconcatrn  43693  naddgeoa  43745  mnuop3d  44621  fvelsetpreimafv  47741  opnneir  49260