Theorem reximdv 3180

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 3176	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  r19.12  3314  ss2rexv  4010  reusv3  5378  fvelima  6948  iunpw  7771  frxp  8123  nnaordex2  8626  ssfiALT  9159  ordtypelem2  9482  wdom2d  9543  xpwdomg  9548  cff1  10243  iunfo  10524  nqereu  10915  reclem3pr  11035  map2psrpr  11096  supsrlem  11097  1re  11209  elss2prb  14527  exprelprel  14529  o1lo1  15590  rlimcn1  15641  subcn2  15648  lo1add  15680  lo1mul  15681  pythagtriplem19  16894  vdwnnlem2  17057  ramub2  17075  sylow2alem2  19689  lsmless2x  19716  efgrelexlemb  19821  scmateALT  22650  decpmatmulsumfsupp  22911  pmatcollpw1lem1  22912  pmatcollpw2lem  22915  pm2mpmhmlem1  22956  cpmidpmatlem3  23010  cpmidgsum2  23017  tgcl  23107  neiss  23247  ssnei2  23254  tgcnp  23391  cnpco  23405  cnpresti  23426  lmcnp  23442  hausnei2  23491  1stcrest  23591  nlly2i  23614  llyss  23617  nllyss  23618  reftr  23652  lfinun  23663  txcnpi  23746  txcmplem1  23779  tx1stc  23788  nrmr0reg  23887  fbssfi  23975  fbfinnfr  23979  fgcl  24016  ufinffr  24067  elfm2  24086  fmfnfmlem1  24092  fmco  24099  fbflim2  24115  flffbas  24133  flftg  24134  cnpflf2  24138  alexsubALT  24189  cnextcn  24205  isucn2  24416  ucnima  24418  blssexps  24564  blssex  24565  mopni3  24632  neibl  24639  metss  24646  metcnp3  24678  cfilucfil  24697  metustbl  24704  psmetutop  24705  mpomulcn  25007  rescncf  25037  lebnum  25104  xlebnum  25105  lebnumii  25106  lmmbr  25398  fgcfil  25411  ovolsslem  25624  ovolunlem1  25637  ovoliunnul  25647  itgcn  25985  ellimc3  26019  c1lip3  26139  itgsubstlem  26188  plyss  26337  ulmclm  26531  ulmcau  26539  ulmcn  26543  rlimcxp  27119  chtppilimlem2  27619  chtppilim  27620  madess  28040  lrrecfr  28117  midex  28999  umgrnloop0  29440  usgrnloop0ALT  29536  uhgr2edg  29539  vtxduhgr0nedg  29823  wlkonl1iedg  29994  elwspths2on  30292  elwspths2onw  30293  3cyclfrgrrn2  30619  isgrpo  30830  tpr2rico  34283  esumpcvgval  34449  omssubadd  34671  r1filim  35479  fineqvnttrclse  35518  vonf1oonfo  35580  connpconn  35708  cvmliftlem15  35771  cvmlift2lem10  35785  satfdmlem  35841  fmla1  35860  satffunlem1lem2  35876  satffunlem2lem2  35879  fnessref  36849  ttctr  36985  fvineqsneq  38039  pibt2  38044  ptrecube  38252  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  fdc1  38378  sstotbnd3  38408  totbndss  38409  heibor1lem  38441  heibor1  38442  opidonOLD  38484  rngmgmbs4  38563  lvoli2  40336  paddss2  40573  lhpexle1lem  40762  lhpexle2lem  40764  dvhdimlem  42199  dvh3dim3N  42204  mapdh9a  42544  hdmap11lem2  42597  fiphp3d  43529  pell1qrss14  43578  minregex  44243  mnuop3d  44964  grumnudlem  44978  ismnushort  44994  eliuniin  45800  restuni3  45819  eliuniin2  45821  disjrnmpt2  45889  rnmptbd2lem  45946  ssfiunibd  46011  supminfxrrnmpt  46168  climrec  46302  islptre  46318  lptre2pt  46337  limsupmnfuzlem  46423  limsupre3lem  46429  limsupvaluz2  46435  supcnvlimsup  46437  liminfvalxr  46480  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  stoweidlem27  46724  stoweidlem29  46726  stoweidlem35  46732  stoweidlem48  46745  stoweidlem62  46759  fourierdlem48  46851  fourierdlem64  46867  fourierdlem65  46868  fourierdlem71  46874  fourierdlem73  46876  fourierdlem94  46897  fourierdlem103  46906  fourierdlem104  46907  fourierdlem112  46915  fourierdlem113  46916  sge0isum  47124  sge0seq  47143  meaiuninclem  47177  carageniuncllem2  47219  ovnsslelem  47257  hoidmvlelem1  47292  2reuimp  47835  afvelima  47887  sgoldbeven3prm  48531  nnsum4primes4  48537  nnsum4primesprm  48539  nnsum4primesgbe  48541  nnsum4primesle9  48543  grtriprop  48689  pgrpgt2nabl  49129  opnneilv  49670  sepnsepo  49685