Theorem reximdv2 3150

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3061

This theorem is referenced by:  reximdvai  3151  reximssdv  3158  ssrexvOLD  4032  ssimaex  6964  nnsuc  7879  oaass  8573  omeulem1  8594  ssnnfi  9183  findcard3  9290  findcard3OLD  9291  unfilem1  9315  epfrs  9745  alephval3  10124  isfin7-2  10410  fpwwe2lem12  10656  inawinalem  10703  ico0  13408  ioc0  13409  r19.2uz  15370  climrlim2  15563  prmdvdsncoprmbd  16746  iserodd  16855  ramub2  17034  prmgaplem6  17076  ghmqusnsglem2  19264  ghmquskerlem2  19268  ablfaclem3  20070  unitgrp  20343  restnlly  23420  llyrest  23423  nllyrest  23424  llyidm  23426  nllyidm  23427  cnpflfi  23937  cnextcn  24005  ivthlem3  25406  dvfsumrlim  25990  lgsquadlem2  27344  oppperpex  28732  outpasch  28734  ushgredgedg  29208  ushgredgedgloop  29210  cusgrfilem2  29436  nsgqusf1olem2  33429  ssmxidl  33489  cmppcmp  33889  eulerpartlemgvv  34408  eulerpartlemgh  34410  fnrelpredd  35120  erdszelem7  35219  rellysconn  35273  ivthALT  36353  fnessref  36375  phpreu  37628  poimirlem26  37670  itg2gt0cn  37699  frinfm  37759  sstotbnd2  37798  heiborlem3  37837  isdrngo3  37983  dihjat1lem  41447  dvh1dim  41461  dochsatshp  41470  mapdpglem2  41692  prjspreln0  42632  pellexlem5  42856  pell14qrss1234  42879  pell1qrss14  42891  lnr2i  43140  hbtlem6  43153  dflim5  43353  tfsconcatrn  43366  naddgeoa  43418  mnuop3d  44295  fvelsetpreimafv  47401  opnneir  48881