Theorem reximdv 3151

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 25	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3147	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3060

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 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  r19.12  3285  ss2rexv  4005  reusv3  5350  fvelima  6899  iunpw  7716  frxp  8068  nnaordex2  8567  ssfiALT  9098  ordtypelem2  9424  wdom2d  9485  xpwdomg  9490  cff1  10168  iunfo  10449  nqereu  10840  reclem3pr  10960  map2psrpr  11021  supsrlem  11022  1re  11132  elss2prb  14411  exprelprel  14413  o1lo1  15460  rlimcn1  15511  subcn2  15518  lo1add  15550  lo1mul  15551  pythagtriplem19  16761  vdwnnlem2  16924  ramub2  16942  sylow2alem2  19547  lsmless2x  19574  efgrelexlemb  19679  scmateALT  22456  decpmatmulsumfsupp  22717  pmatcollpw1lem1  22718  pmatcollpw2lem  22721  pm2mpmhmlem1  22762  cpmidpmatlem3  22816  cpmidgsum2  22823  tgcl  22913  neiss  23053  ssnei2  23060  tgcnp  23197  cnpco  23211  cnpresti  23232  lmcnp  23248  hausnei2  23297  1stcrest  23397  nlly2i  23420  llyss  23423  nllyss  23424  reftr  23458  lfinun  23469  txcnpi  23552  txcmplem1  23585  tx1stc  23594  nrmr0reg  23693  fbssfi  23781  fbfinnfr  23785  fgcl  23822  ufinffr  23873  elfm2  23892  fmfnfmlem1  23898  fmco  23905  fbflim2  23921  flffbas  23939  flftg  23940  cnpflf2  23944  alexsubALT  23995  cnextcn  24011  isucn2  24222  ucnima  24224  blssexps  24370  blssex  24371  mopni3  24438  neibl  24445  metss  24452  metcnp3  24484  cfilucfil  24503  metustbl  24510  psmetutop  24511  mpomulcn  24814  rescncf  24846  lebnum  24919  xlebnum  24920  lebnumii  24921  lmmbr  25214  fgcfil  25227  ovolsslem  25441  ovolunlem1  25454  ovoliunnul  25464  itgcn  25802  ellimc3  25836  c1lip3  25960  itgsubstlem  26011  plyss  26160  ulmclm  26352  ulmcau  26360  ulmcn  26364  rlimcxp  26940  chtppilimlem2  27441  chtppilim  27442  madess  27862  lrrecfr  27939  midex  28809  umgrnloop0  29182  usgrnloop0ALT  29278  uhgr2edg  29281  vtxduhgr0nedg  29566  wlkonl1iedg  29737  elwspths2on  30035  elwspths2onw  30036  3cyclfrgrrn2  30362  isgrpo  30572  tpr2rico  34069  esumpcvgval  34235  omssubadd  34457  r1filim  35260  fineqvnttrclse  35280  connpconn  35429  cvmliftlem15  35492  cvmlift2lem10  35506  satfdmlem  35562  fmla1  35581  satffunlem1lem2  35597  satffunlem2lem2  35600  fnessref  36551  fvineqsneq  37617  pibt2  37622  ptrecube  37821  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  fdc1  37947  sstotbnd3  37977  totbndss  37978  heibor1lem  38010  heibor1  38011  opidonOLD  38053  rngmgmbs4  38132  lvoli2  39841  paddss2  40078  lhpexle1lem  40267  lhpexle2lem  40269  dvhdimlem  41704  dvh3dim3N  41709  mapdh9a  42049  hdmap11lem2  42102  fiphp3d  43061  pell1qrss14  43110  minregex  43775  mnuop3d  44512  grumnudlem  44526  ismnushort  44542  eliuniin  45343  restuni3  45362  eliuniin2  45364  disjrnmpt2  45432  rnmptbd2lem  45492  ssfiunibd  45557  supminfxrrnmpt  45715  climrec  45849  islptre  45865  lptre2pt  45884  limsupmnfuzlem  45970  limsupre3lem  45976  limsupvaluz2  45982  supcnvlimsup  45984  liminfvalxr  46027  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  stoweidlem27  46271  stoweidlem29  46273  stoweidlem35  46279  stoweidlem48  46292  stoweidlem62  46306  fourierdlem48  46398  fourierdlem64  46414  fourierdlem65  46415  fourierdlem71  46421  fourierdlem73  46423  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fourierdlem113  46463  sge0isum  46671  sge0seq  46690  meaiuninclem  46724  carageniuncllem2  46766  ovnsslelem  46804  hoidmvlelem1  46839  2reuimp  47361  afvelima  47413  sgoldbeven3prm  48029  nnsum4primes4  48035  nnsum4primesprm  48037  nnsum4primesgbe  48039  nnsum4primesle9  48041  grtriprop  48187  pgrpgt2nabl  48612  opnneilv  49154  sepnsepo  49169