Theorem reximdv 3181

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  r19.12  3315  ss2rexv  3985  reusv3  5374  fvelima  6981  mpt3fvd  7720  iunpw  7817  frxp  8175  nnaordex2  8686  ssfiALT  9227  ordtypelem2  9550  wdom2d  9611  xpwdomg  9616  elhf4  9949  cff1  10375  iunfo  10662  nqereu  11053  reclem3pr  11173  map2psrpr  11234  supsrlem  11235  1re  11347  elss2prb  14674  exprelprel  14676  o1lo1  15748  rlimcn1  15799  subcn2  15806  lo1add  15838  lo1mul  15839  pythagtriplem19  17055  vdwnnlem2  17218  ramub2  17236  mgmidpfod  18907  sylow2alem2  19883  lsmless2x  19910  efgrelexlemb  20015  scmateALT  22882  decpmatmulsumfsupp  23146  pmatcollpw1lem1  23147  pmatcollpw2lem  23150  pm2mpmhmlem1  23191  cpmidpmatlem3  23245  cpmidgsum2  23252  tgcl  23342  neiss  23482  ssnei2  23489  tgcnp  23626  cnpco  23640  cnpresti  23661  lmcnp  23677  hausnei2  23726  1stcrest  23826  nlly2i  23850  llyss  23853  nllyss  23854  reftr  23888  lfinun  23899  txcnpi  23982  txcmplem1  24015  tx1stc  24024  nrmr0reg  24123  fbssfi  24211  fbfinnfr  24215  fgcl  24252  ufinffr  24303  elfm2  24322  fmfnfmlem1  24328  fmco  24335  fbflim2  24351  flffbas  24369  flftg  24370  cnpflf2  24374  alexsubALT  24425  cnextcn  24441  isucn2  24652  ucnima  24654  blssexps  24800  blssex  24801  mopni3  24868  neibl  24875  metss  24882  metcnp3  24914  cfilucfil  24933  metustbl  24940  psmetutop  24941  mpomulcn  25243  rescncf  25273  lebnum  25340  xlebnum  25341  lebnumii  25342  lmmbr  25634  fgcfil  25647  ovolsslem  25860  ovolunlem1  25873  ovoliunnul  25883  itgcn  26220  ellimc3  26254  c1lip3  26374  itgsubstlem  26423  plyss  26572  ulmclm  26771  ulmcau  26779  ulmcn  26783  rlimcxp  27358  chtppilimlem2  27858  chtppilim  27859  madess  28309  lrrecfr  28386  midex  29270  umgrnloop0  29744  usgrnloop0ALT  29843  uhgr2edg  29846  vtxduhgr0nedg  30130  wlkonl1iedg  30301  elwspths2on  30608  elwspths2onw  30609  3cyclfrgrrn2  30945  isgrpo  31156  tpr2rico  34655  esumpcvgval  34821  omssubadd  35043  r1filim  35854  fineqvnttrclse  35933  jf1o  36052  vonf1oonfo  36090  connpconn  36208  cvmliftlem15  36271  cvmlift2lem10  36285  satfdmlem  36341  fmla1  36360  satffunlem1lem2  36376  satffunlem2lem2  36379  fnessref  37360  ttctr  37496  fvineqsneq  38603  pibt2  38608  ptrecube  38806  poimirlem29  38835  poimirlem30  38836  poimirlem31  38837  dfprop2  38914  fdc1  38946  sstotbnd3  38976  totbndss  38977  heibor1lem  39009  heibor1  39010  opidonOLD  39052  rngmgmbs4  39131  lvoli2  40904  paddss2  41141  lhpexle1lem  41330  lhpexle2lem  41332  dvhdimlem  42767  dvh3dim3N  42772  mapdh9a  43112  hdmap11lem2  43165  fiphp3d  44092  pell1qrss14  44141  minregex  44796  mnuop3d  45516  grumnudlem  45530  ismnushort  45546  eliuniin  46387  restuni3  46406  eliuniin2  46408  disjrnmpt2  46476  rnmptbd2lem  46533  ssfiunibd  46598  supminfxrrnmpt  46754  climrec  46888  islptre  46904  lptre2pt  46923  limsupmnfuzlem  47009  limsupre3lem  47015  limsupvaluz2  47021  supcnvlimsup  47023  liminfvalxr  47066  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  stoweidlem27  47310  stoweidlem29  47312  stoweidlem35  47318  stoweidlem48  47331  stoweidlem62  47345  fourierdlem48  47437  fourierdlem64  47453  fourierdlem65  47454  fourierdlem71  47460  fourierdlem73  47462  fourierdlem94  47483  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  fourierdlem113  47502  sge0isum  47710  sge0seq  47729  meaiuninclem  47763  carageniuncllem2  47805  ovnsslelem  47843  hoidmvlelem1  47878  2reuimp  48459  afvelima  48510  sgoldbeven3prm  49154  nnsum4primes4  49160  nnsum4primesprm  49162  nnsum4primesgbe  49164  nnsum4primesle9  49166  grtriprop  49312  pgrpgt2nabl  49809  opnneilv  50354  sepnsepo  50369