MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximdv Structured version   Visualization version   GIF version

Theorem reximdv 3278
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
reximdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
reximdv (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv
StepHypRef Expression
1 reximdv.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 3277 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wrex 3144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-ral 3148  df-rex 3149
This theorem is referenced by:  r19.12  3329  r19.12OLD  3332  ss2rexv  4040  reusv3  5302  fvelima  6728  iunpw  7481  frxp  7811  ssfi  8727  ordtypelem2  8972  wdom2d  9033  xpwdomg  9038  cff1  9669  iunfo  9950  nqereu  10340  reclem3pr  10460  map2psrpr  10521  supsrlem  10522  1re  10630  elss2prb  13835  exprelprel  13837  o1lo1  14884  rlimcn1  14935  subcn2  14941  lo1add  14973  lo1mul  14974  pythagtriplem19  16160  vdwnnlem2  16322  ramub2  16340  sylow2alem2  18663  lsmless2x  18690  efgrelexlemb  18796  scmateALT  21037  decpmatmulsumfsupp  21297  pmatcollpw1lem1  21298  pmatcollpw2lem  21301  pm2mpmhmlem1  21342  cpmidpmatlem3  21396  cpmidgsum2  21403  tgcl  21493  neiss  21633  ssnei2  21640  tgcnp  21777  cnpco  21791  cnpresti  21812  lmcnp  21828  hausnei2  21877  1stcrest  21977  nlly2i  22000  llyss  22003  nllyss  22004  reftr  22038  lfinun  22049  txcnpi  22132  txcmplem1  22165  tx1stc  22174  nrmr0reg  22273  fbssfi  22361  fbfinnfr  22365  fgcl  22402  ufinffr  22453  elfm2  22472  fmfnfmlem1  22478  fmco  22485  fbflim2  22501  flffbas  22519  flftg  22520  cnpflf2  22524  alexsubALT  22575  cnextcn  22591  isucn2  22803  ucnima  22805  blssexps  22951  blssex  22952  mopni3  23019  neibl  23026  metss  23033  metcnp3  23065  cfilucfil  23084  metustbl  23091  psmetutop  23092  rescncf  23420  lebnum  23483  xlebnum  23484  lebnumii  23485  lmmbr  23776  fgcfil  23789  ovolsslem  24000  ovolunlem1  24013  ovoliunnul  24023  itgcn  24358  ellimc3  24392  c1lip3  24511  itgsubstlem  24560  plyss  24704  ulmclm  24890  ulmcau  24898  ulmcn  24902  rlimcxp  25465  chtppilimlem2  25964  chtppilim  25965  midex  26437  umgrnloop0  26808  usgrnloop0ALT  26901  uhgr2edg  26904  vtxduhgr0nedg  27188  wlkonl1iedg  27361  elwspths2on  27653  3cyclfrgrrn2  27980  isgrpo  28188  tpr2rico  31041  esumpcvgval  31223  omssubadd  31444  connpconn  32366  cvmliftlem15  32429  cvmlift2lem10  32443  satfdmlem  32499  fmla1  32518  satffunlem1lem2  32534  satffunlem2lem2  32537  fnessref  33589  fvineqsneq  34562  pibt2  34567  ptrecube  34759  poimirlem29  34788  poimirlem30  34789  poimirlem31  34790  fdc1  34889  sstotbnd3  34922  totbndss  34923  heibor1lem  34955  heibor1  34956  opidonOLD  34998  rngmgmbs4  35077  lvoli2  36584  paddss2  36821  lhpexle1lem  37010  lhpexle2lem  37012  dvhdimlem  38447  dvh3dim3N  38452  mapdh9a  38792  hdmap11lem2  38845  fiphp3d  39281  pell1qrss14  39330  mnuop3d  40472  grumnudlem  40486  eliuniin  41230  restuni3  41250  eliuniin2  41252  disjrnmpt2  41314  rnmptbd2lem  41385  ssfiunibd  41441  supminfxrrnmpt  41612  climrec  41749  islptre  41765  lptre2pt  41786  limsupmnfuzlem  41872  limsupre3lem  41878  limsupvaluz2  41884  supcnvlimsup  41886  liminfvalxr  41929  ioodvbdlimc1lem2  42082  ioodvbdlimc2lem  42084  stoweidlem27  42178  stoweidlem29  42180  stoweidlem35  42186  stoweidlem48  42199  stoweidlem62  42213  fourierdlem48  42305  fourierdlem64  42321  fourierdlem65  42322  fourierdlem71  42328  fourierdlem73  42330  fourierdlem94  42351  fourierdlem103  42360  fourierdlem104  42361  fourierdlem112  42369  fourierdlem113  42370  sge0isum  42575  sge0seq  42594  meaiuninclem  42628  carageniuncllem2  42670  ovnsslelem  42708  hoidmvlelem1  42743  2reuimp  43180  afvelima  43232  sgoldbeven3prm  43780  nnsum4primes4  43786  nnsum4primesprm  43788  nnsum4primesgbe  43790  nnsum4primesle9  43792  pgrpgt2nabl  44246
  Copyright terms: Public domain W3C validator