Theorem reximdv2 3144

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054

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 3055

This theorem is referenced by:  reximdvai  3145  reximssdv  3152  ssrexvOLD  4023  ssimaex  6949  nnsuc  7863  oaass  8528  omeulem1  8549  ssnnfi  9139  findcard3  9236  findcard3OLD  9237  unfilem1  9261  epfrs  9691  alephval3  10070  isfin7-2  10356  fpwwe2lem12  10602  inawinalem  10649  ico0  13359  ioc0  13360  r19.2uz  15325  climrlim2  15520  prmdvdsncoprmbd  16704  iserodd  16813  ramub2  16992  prmgaplem6  17034  ghmqusnsglem2  19220  ghmquskerlem2  19224  ablfaclem3  20026  unitgrp  20299  restnlly  23376  llyrest  23379  nllyrest  23380  llyidm  23382  nllyidm  23383  cnpflfi  23893  cnextcn  23961  ivthlem3  25361  dvfsumrlim  25945  lgsquadlem2  27299  oppperpex  28687  outpasch  28689  ushgredgedg  29163  ushgredgedgloop  29165  cusgrfilem2  29391  nsgqusf1olem2  33392  ssmxidl  33452  cmppcmp  33855  eulerpartlemgvv  34374  eulerpartlemgh  34376  fnrelpredd  35086  erdszelem7  35191  rellysconn  35245  ivthALT  36330  fnessref  36352  phpreu  37605  poimirlem26  37647  itg2gt0cn  37676  frinfm  37736  sstotbnd2  37775  heiborlem3  37814  isdrngo3  37960  dihjat1lem  41429  dvh1dim  41443  dochsatshp  41452  mapdpglem2  41674  prjspreln0  42604  pellexlem5  42828  pell14qrss1234  42851  pell1qrss14  42863  lnr2i  43112  hbtlem6  43125  dflim5  43325  tfsconcatrn  43338  naddgeoa  43390  mnuop3d  44267  fvelsetpreimafv  47392  opnneir  48899