Theorem reximdv2 3194

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

Syntax hints:   → wi 4   ∧ wa 386  ∃wex 1823   ∈ wcel 2106  ∃wrex 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-ex 1824  df-rex 3095

This theorem is referenced by:  reximssdv  3199  ssrexv  3885  ssimaex  6523  nnsuc  7360  oaass  7925  omeulem1  7946  ssnnfi  8467  findcard3  8491  unfilem1  8512  epfrs  8904  alephval3  9266  isfin7-2  9553  fpwwe2lem13  9799  inawinalem  9846  ico0  12533  ioc0  12534  r19.2uz  14498  climrlim2  14686  iserodd  15944  ramub2  16122  prmgaplem6  16164  ablfaclem3  18873  unitgrp  19054  restnlly  21694  llyrest  21697  nllyrest  21698  llyidm  21700  nllyidm  21701  cnpflfi  22211  cnextcn  22279  ivthlem3  23657  dvfsumrlim  24231  lgsquadlem2  25558  footex  26069  oppperpex  26101  outpasch  26103  ushgredgedg  26575  ushgredgedgloop  26577  ushgredgedgloopOLD  26578  cusgrfilem2  26804  cmppcmp  30523  eulerpartlemgvv  31036  eulerpartlemgh  31038  erdszelem7  31778  rellysconn  31832  trpredrec  32326  ivthALT  32918  fnessref  32940  phpreu  34002  poimirlem26  34045  itg2gt0cn  34074  frinfm  34139  sstotbnd2  34181  heiborlem3  34220  isdrngo3  34366  dihjat1lem  37566  dvh1dim  37580  dochsatshp  37589  mapdpglem2  37811  pellexlem5  38339  pell14qrss1234  38362  pell1qrss14  38374  lnr2i  38627  hbtlem6  38640