Theorem reximdv 3153

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

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

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 3063

This theorem is referenced by:  r19.12  3287  ss2rexv  3994  reusv3  5342  fvelima  6899  iunpw  7718  frxp  8069  nnaordex2  8568  ssfiALT  9101  ordtypelem2  9427  wdom2d  9488  xpwdomg  9493  cff1  10171  iunfo  10452  nqereu  10843  reclem3pr  10963  map2psrpr  11024  supsrlem  11025  1re  11135  elss2prb  14441  exprelprel  14443  o1lo1  15490  rlimcn1  15541  subcn2  15548  lo1add  15580  lo1mul  15581  pythagtriplem19  16795  vdwnnlem2  16958  ramub2  16976  sylow2alem2  19584  lsmless2x  19611  efgrelexlemb  19716  scmateALT  22487  decpmatmulsumfsupp  22748  pmatcollpw1lem1  22749  pmatcollpw2lem  22752  pm2mpmhmlem1  22793  cpmidpmatlem3  22847  cpmidgsum2  22854  tgcl  22944  neiss  23084  ssnei2  23091  tgcnp  23228  cnpco  23242  cnpresti  23263  lmcnp  23279  hausnei2  23328  1stcrest  23428  nlly2i  23451  llyss  23454  nllyss  23455  reftr  23489  lfinun  23500  txcnpi  23583  txcmplem1  23616  tx1stc  23625  nrmr0reg  23724  fbssfi  23812  fbfinnfr  23816  fgcl  23853  ufinffr  23904  elfm2  23923  fmfnfmlem1  23929  fmco  23936  fbflim2  23952  flffbas  23970  flftg  23971  cnpflf2  23975  alexsubALT  24026  cnextcn  24042  isucn2  24253  ucnima  24255  blssexps  24401  blssex  24402  mopni3  24469  neibl  24476  metss  24483  metcnp3  24515  cfilucfil  24534  metustbl  24541  psmetutop  24542  mpomulcn  24844  rescncf  24874  lebnum  24941  xlebnum  24942  lebnumii  24943  lmmbr  25235  fgcfil  25248  ovolsslem  25461  ovolunlem1  25474  ovoliunnul  25484  itgcn  25822  ellimc3  25856  c1lip3  25976  itgsubstlem  26025  plyss  26174  ulmclm  26365  ulmcau  26373  ulmcn  26377  rlimcxp  26951  chtppilimlem2  27451  chtppilim  27452  madess  27872  lrrecfr  27949  midex  28819  umgrnloop0  29192  usgrnloop0ALT  29288  uhgr2edg  29291  vtxduhgr0nedg  29576  wlkonl1iedg  29747  elwspths2on  30045  elwspths2onw  30046  3cyclfrgrrn2  30372  isgrpo  30583  tpr2rico  34072  esumpcvgval  34238  omssubadd  34460  r1filim  35263  fineqvnttrclse  35284  connpconn  35433  cvmliftlem15  35496  cvmlift2lem10  35510  satfdmlem  35566  fmla1  35585  satffunlem1lem2  35601  satffunlem2lem2  35604  fnessref  36555  ttctr  36691  fvineqsneq  37742  pibt2  37747  ptrecube  37955  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  fdc1  38081  sstotbnd3  38111  totbndss  38112  heibor1lem  38144  heibor1  38145  opidonOLD  38187  rngmgmbs4  38266  lvoli2  40041  paddss2  40278  lhpexle1lem  40467  lhpexle2lem  40469  dvhdimlem  41904  dvh3dim3N  41909  mapdh9a  42249  hdmap11lem2  42302  fiphp3d  43265  pell1qrss14  43314  minregex  43979  mnuop3d  44716  grumnudlem  44730  ismnushort  44746  eliuniin  45547  restuni3  45566  eliuniin2  45568  disjrnmpt2  45636  rnmptbd2lem  45695  ssfiunibd  45760  supminfxrrnmpt  45917  climrec  46051  islptre  46067  lptre2pt  46086  limsupmnfuzlem  46172  limsupre3lem  46178  limsupvaluz2  46184  supcnvlimsup  46186  liminfvalxr  46229  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem27  46473  stoweidlem29  46475  stoweidlem35  46481  stoweidlem48  46494  stoweidlem62  46508  fourierdlem48  46600  fourierdlem64  46616  fourierdlem65  46617  fourierdlem71  46623  fourierdlem73  46625  fourierdlem94  46646  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fourierdlem113  46665  sge0isum  46873  sge0seq  46892  meaiuninclem  46926  carageniuncllem2  46968  ovnsslelem  47006  hoidmvlelem1  47041  2reuimp  47575  afvelima  47627  sgoldbeven3prm  48271  nnsum4primes4  48277  nnsum4primesprm  48279  nnsum4primesgbe  48281  nnsum4primesle9  48283  grtriprop  48429  pgrpgt2nabl  48854  opnneilv  49396  sepnsepo  49411