Theorem reximdv2 3172

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812  df-rex 3087

This theorem is used by:  reximdvai  3173  reximssdv  3180  ssimaex  6971  nnsuc  7896  oaass  8573  omeulem1  8594  ssnnfi  9189  findcard3  9278  unfilem1  9301  epfrs  9736  r1filimi  9907  alephval3  10193  isfin7-2  10478  fpwwe2lem12  10731  inawinalem  10778  ico0  13526  ioc0  13527  r19.2uz  15525  climrlim2  15720  prmdvdsncoprmbd  16909  iserodd  17019  ramub2  17198  prmgaplem6  17240  ghmqusnsglem2  19501  ghmquskerlem2  19505  ablfaclem3  20309  unitgrp  20619  isdrng5  21014  restnlly  23807  llyrest  23810  nllyrest  23811  llyidm  23813  nllyidm  23814  cnpflfi  24324  cnextcn  24392  ivthlem3  25780  dvfsumrlim  26357  lgsquadlem2  27714  tglnpt3  29128  tglnpt4  29129  oppperpex  29235  outpasch  29239  ushgredgedg  29816  ushgredgedgloop  29818  cusgrfilem2  30043  nsgqusf1olem2  34012  ssmxidl  34046  cmppcmp  34537  eulerpartlemgvv  35055  eulerpartlemgh  35057  fnrelpredd  35773  noinfepfnregs  35857  erdszelem7  36049  rellysconn  36103  ivthALT  37216  fnessref  37238  phpreu  38621  poimirlem26  38658  itg2gt0cn  38687  frinfm  38763  sstotbnd2  38802  heiborlem3  38841  isdrngo3  38987  dihjat1lem  42579  dvh1dim  42593  dochsatshp  42602  mapdpglem2  42824  prjspreln0  43731  pellexlem5  43934  pell14qrss1234  43957  pell1qrss14  43969  lnr2i  44212  hbtlem6  44225  dflim5  44425  tfsconcatrn  44438  naddgeoa  44490  mnuop3d  45349  fvelsetpreimafv  48563  opnneir  50115