Theorem reximdv 3186

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3182	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  r19.12  3320  ss2rexv  4017  reusv3  5374  fvelima  6944  iunpw  7766  frxp  8118  nnaordex2  8621  ssfiALT  9154  ordtypelem2  9477  wdom2d  9538  xpwdomg  9543  cff1  10238  iunfo  10519  nqereu  10910  reclem3pr  11030  map2psrpr  11091  supsrlem  11092  1re  11204  elss2prb  14521  exprelprel  14523  o1lo1  15584  rlimcn1  15635  subcn2  15642  lo1add  15674  lo1mul  15675  pythagtriplem19  16889  vdwnnlem2  17052  ramub2  17070  sylow2alem2  19684  lsmless2x  19711  efgrelexlemb  19816  scmateALT  22634  decpmatmulsumfsupp  22895  pmatcollpw1lem1  22896  pmatcollpw2lem  22899  pm2mpmhmlem1  22940  cpmidpmatlem3  22994  cpmidgsum2  23001  tgcl  23091  neiss  23231  ssnei2  23238  tgcnp  23375  cnpco  23389  cnpresti  23410  lmcnp  23426  hausnei2  23475  1stcrest  23575  nlly2i  23598  llyss  23601  nllyss  23602  reftr  23636  lfinun  23647  txcnpi  23730  txcmplem1  23763  tx1stc  23772  nrmr0reg  23871  fbssfi  23959  fbfinnfr  23963  fgcl  24000  ufinffr  24051  elfm2  24070  fmfnfmlem1  24076  fmco  24083  fbflim2  24099  flffbas  24117  flftg  24118  cnpflf2  24122  alexsubALT  24173  cnextcn  24189  isucn2  24400  ucnima  24402  blssexps  24548  blssex  24549  mopni3  24616  neibl  24623  metss  24630  metcnp3  24662  cfilucfil  24681  metustbl  24688  psmetutop  24689  mpomulcn  24991  rescncf  25021  lebnum  25088  xlebnum  25089  lebnumii  25090  lmmbr  25382  fgcfil  25395  ovolsslem  25608  ovolunlem1  25621  ovoliunnul  25631  itgcn  25969  ellimc3  26003  c1lip3  26123  itgsubstlem  26172  plyss  26321  ulmclm  26512  ulmcau  26520  ulmcn  26524  rlimcxp  27100  chtppilimlem2  27600  chtppilim  27601  madess  28021  lrrecfr  28098  midex  28973  umgrnloop0  29396  usgrnloop0ALT  29492  uhgr2edg  29495  vtxduhgr0nedg  29779  wlkonl1iedg  29950  elwspths2on  30248  elwspths2onw  30249  3cyclfrgrrn2  30575  isgrpo  30786  tpr2rico  34243  esumpcvgval  34409  omssubadd  34631  r1filim  35436  fineqvnttrclse  35456  vonf1oonfo  35494  connpconn  35622  cvmliftlem15  35685  cvmlift2lem10  35699  satfdmlem  35755  fmla1  35774  satffunlem1lem2  35790  satffunlem2lem2  35793  fnessref  36753  ttctr  36889  fvineqsneq  37941  pibt2  37946  ptrecube  38154  poimirlem29  38183  poimirlem30  38184  poimirlem31  38185  fdc1  38280  sstotbnd3  38310  totbndss  38311  heibor1lem  38343  heibor1  38344  opidonOLD  38386  rngmgmbs4  38465  lvoli2  40240  paddss2  40477  lhpexle1lem  40666  lhpexle2lem  40668  dvhdimlem  42103  dvh3dim3N  42108  mapdh9a  42448  hdmap11lem2  42501  fiphp3d  43431  pell1qrss14  43480  minregex  44145  mnuop3d  44866  grumnudlem  44880  ismnushort  44896  eliuniin  45702  restuni3  45721  eliuniin2  45723  disjrnmpt2  45791  rnmptbd2lem  45848  ssfiunibd  45913  supminfxrrnmpt  46070  climrec  46204  islptre  46220  lptre2pt  46239  limsupmnfuzlem  46325  limsupre3lem  46331  limsupvaluz2  46337  supcnvlimsup  46339  liminfvalxr  46382  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  stoweidlem27  46626  stoweidlem29  46628  stoweidlem35  46634  stoweidlem48  46647  stoweidlem62  46661  fourierdlem48  46753  fourierdlem64  46769  fourierdlem65  46770  fourierdlem71  46776  fourierdlem73  46778  fourierdlem94  46799  fourierdlem103  46808  fourierdlem104  46809  fourierdlem112  46817  fourierdlem113  46818  sge0isum  47026  sge0seq  47045  meaiuninclem  47079  carageniuncllem2  47121  ovnsslelem  47159  hoidmvlelem1  47194  2reuimp  47734  afvelima  47786  sgoldbeven3prm  48430  nnsum4primes4  48436  nnsum4primesprm  48438  nnsum4primesgbe  48440  nnsum4primesle9  48442  grtriprop  48588  pgrpgt2nabl  49024  opnneilv  49565  sepnsepo  49580