Theorem reximdv 3152

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  r19.12  3286  ss2rexv  3993  reusv3  5347  fvelima  6905  iunpw  7725  frxp  8076  nnaordex2  8575  ssfiALT  9108  ordtypelem2  9434  wdom2d  9495  xpwdomg  9500  cff1  10180  iunfo  10461  nqereu  10852  reclem3pr  10972  map2psrpr  11033  supsrlem  11034  1re  11144  elss2prb  14450  exprelprel  14452  o1lo1  15499  rlimcn1  15550  subcn2  15557  lo1add  15589  lo1mul  15590  pythagtriplem19  16804  vdwnnlem2  16967  ramub2  16985  sylow2alem2  19593  lsmless2x  19620  efgrelexlemb  19725  scmateALT  22477  decpmatmulsumfsupp  22738  pmatcollpw1lem1  22739  pmatcollpw2lem  22742  pm2mpmhmlem1  22783  cpmidpmatlem3  22837  cpmidgsum2  22844  tgcl  22934  neiss  23074  ssnei2  23081  tgcnp  23218  cnpco  23232  cnpresti  23253  lmcnp  23269  hausnei2  23318  1stcrest  23418  nlly2i  23441  llyss  23444  nllyss  23445  reftr  23479  lfinun  23490  txcnpi  23573  txcmplem1  23606  tx1stc  23615  nrmr0reg  23714  fbssfi  23802  fbfinnfr  23806  fgcl  23843  ufinffr  23894  elfm2  23913  fmfnfmlem1  23919  fmco  23926  fbflim2  23942  flffbas  23960  flftg  23961  cnpflf2  23965  alexsubALT  24016  cnextcn  24032  isucn2  24243  ucnima  24245  blssexps  24391  blssex  24392  mopni3  24459  neibl  24466  metss  24473  metcnp3  24505  cfilucfil  24524  metustbl  24531  psmetutop  24532  mpomulcn  24834  rescncf  24864  lebnum  24931  xlebnum  24932  lebnumii  24933  lmmbr  25225  fgcfil  25238  ovolsslem  25451  ovolunlem1  25464  ovoliunnul  25474  itgcn  25812  ellimc3  25846  c1lip3  25966  itgsubstlem  26015  plyss  26164  ulmclm  26352  ulmcau  26360  ulmcn  26364  rlimcxp  26937  chtppilimlem2  27437  chtppilim  27438  madess  27858  lrrecfr  27935  midex  28805  umgrnloop0  29178  usgrnloop0ALT  29274  uhgr2edg  29277  vtxduhgr0nedg  29561  wlkonl1iedg  29732  elwspths2on  30030  elwspths2onw  30031  3cyclfrgrrn2  30357  isgrpo  30568  tpr2rico  34056  esumpcvgval  34222  omssubadd  34444  r1filim  35247  fineqvnttrclse  35268  connpconn  35417  cvmliftlem15  35480  cvmlift2lem10  35494  satfdmlem  35550  fmla1  35569  satffunlem1lem2  35585  satffunlem2lem2  35588  fnessref  36539  ttctr  36675  fvineqsneq  37728  pibt2  37733  ptrecube  37941  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  fdc1  38067  sstotbnd3  38097  totbndss  38098  heibor1lem  38130  heibor1  38131  opidonOLD  38173  rngmgmbs4  38252  lvoli2  40027  paddss2  40264  lhpexle1lem  40453  lhpexle2lem  40455  dvhdimlem  41890  dvh3dim3N  41895  mapdh9a  42235  hdmap11lem2  42288  fiphp3d  43247  pell1qrss14  43296  minregex  43961  mnuop3d  44698  grumnudlem  44712  ismnushort  44728  eliuniin  45529  restuni3  45548  eliuniin2  45550  disjrnmpt2  45618  rnmptbd2lem  45677  ssfiunibd  45742  supminfxrrnmpt  45899  climrec  46033  islptre  46049  lptre2pt  46068  limsupmnfuzlem  46154  limsupre3lem  46160  limsupvaluz2  46166  supcnvlimsup  46168  liminfvalxr  46211  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem27  46455  stoweidlem29  46457  stoweidlem35  46463  stoweidlem48  46476  stoweidlem62  46490  fourierdlem48  46582  fourierdlem64  46598  fourierdlem65  46599  fourierdlem71  46605  fourierdlem73  46607  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  sge0isum  46855  sge0seq  46874  meaiuninclem  46908  carageniuncllem2  46950  ovnsslelem  46988  hoidmvlelem1  47023  2reuimp  47563  afvelima  47615  sgoldbeven3prm  48259  nnsum4primes4  48265  nnsum4primesprm  48267  nnsum4primesgbe  48269  nnsum4primesle9  48271  grtriprop  48417  pgrpgt2nabl  48842  opnneilv  49384  sepnsepo  49399