Theorem reximdv2 3171

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-rex 3086

This theorem is referenced by:  reximdvai  3172  reximssdv  3179  ssimaex  6948  nnsuc  7860  oaass  8525  omeulem1  8546  ssnnfi  9134  findcard3  9223  unfilem1  9245  epfrs  9683  alephval3  10063  isfin7-2  10350  fpwwe2lem12  10597  inawinalem  10644  ico0  13392  ioc0  13393  r19.2uz  15362  climrlim2  15557  prmdvdsncoprmbd  16745  iserodd  16854  ramub2  17033  prmgaplem6  17075  ghmqusnsglem2  19304  ghmquskerlem2  19308  ablfaclem3  20112  unitgrp  20411  restnlly  23522  llyrest  23525  nllyrest  23526  llyidm  23528  nllyidm  23529  cnpflfi  24039  cnextcn  24107  ivthlem3  25495  dvfsumrlim  26073  lgsquadlem2  27422  oppperpex  28899  outpasch  28901  ushgredgedg  29376  ushgredgedgloop  29378  cusgrfilem2  29603  nsgqusf1olem2  33561  ssmxidl  33623  cmppcmp  34116  eulerpartlemgvv  34634  eulerpartlemgh  34636  fnrelpredd  35351  r1filimi  35363  noinfepfnregs  35392  erdszelem7  35511  rellysconn  35565  ivthALT  36659  fnessref  36681  phpreu  38067  poimirlem26  38109  itg2gt0cn  38138  frinfm  38198  sstotbnd2  38237  heiborlem3  38276  isdrngo3  38422  dihjat1lem  42016  dvh1dim  42030  dochsatshp  42039  mapdpglem2  42261  prjspreln0  43155  pellexlem5  43374  pell14qrss1234  43397  pell1qrss14  43409  lnr2i  43657  hbtlem6  43670  dflim5  43870  tfsconcatrn  43883  naddgeoa  43935  mnuop3d  44811  fvelsetpreimafv  47957  opnneir  49492