Theorem reximdv2 3163

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2105  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 206  df-ex 1781  df-rex 3070

This theorem is referenced by:  reximdvai  3164  reximssdv  3171  ssrexv  4051  ssimaex  6976  nnsuc  7877  oaass  8567  omeulem1  8588  ssnnfi  9175  ssnnfiOLD  9176  findcard3  9291  findcard3OLD  9292  unfilem1  9316  epfrs  9732  alephval3  10111  isfin7-2  10397  fpwwe2lem12  10643  inawinalem  10690  ico0  13377  ioc0  13378  r19.2uz  15305  climrlim2  15498  prmdvdsncoprmbd  16670  iserodd  16775  ramub2  16954  prmgaplem6  16996  ablfaclem3  20005  unitgrp  20281  restnlly  23306  llyrest  23309  nllyrest  23310  llyidm  23312  nllyidm  23313  cnpflfi  23823  cnextcn  23891  ivthlem3  25302  dvfsumrlim  25886  lgsquadlem2  27227  oppperpex  28437  outpasch  28439  ushgredgedg  28919  ushgredgedgloop  28921  cusgrfilem2  29146  nsgqusf1olem2  32965  ghmquskerlem2  32970  ssmxidl  33030  cmppcmp  33302  eulerpartlemgvv  33839  eulerpartlemgh  33841  fnrelpredd  34556  erdszelem7  34652  rellysconn  34706  ivthALT  35684  fnessref  35706  phpreu  36936  poimirlem26  36978  itg2gt0cn  37007  frinfm  37067  sstotbnd2  37106  heiborlem3  37145  isdrngo3  37291  dihjat1lem  40763  dvh1dim  40777  dochsatshp  40786  mapdpglem2  41008  prjspreln0  41814  pellexlem5  42034  pell14qrss1234  42057  pell1qrss14  42069  lnr2i  42321  hbtlem6  42334  dflim5  42542  tfsconcatrn  42555  naddgeoa  42608  mnuop3d  43493  fvelsetpreimafv  46514  opnneir  47701