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

Theorem reximdv 3013
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 3012 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-ral 2914  df-rex 2915
This theorem is referenced by:  r19.12  3059  reusv3  4867  fvelima  6235  iunpw  6963  frxp  7272  ssfi  8165  ordtypelem2  8409  wdom2d  8470  xpwdomg  8475  cff1  9065  iunfo  9346  nqereu  9736  reclem3pr  9856  map2psrpr  9916  supsrlem  9917  1re  10024  elss2prb  13252  exprelprel  13254  o1lo1  14249  rlimcn1  14300  subcn2  14306  lo1add  14338  lo1mul  14339  pythagtriplem19  15519  vdwnnlem2  15681  ramub2  15699  sylow2alem2  18014  lsmless2x  18041  efgrelexlemb  18144  scmateALT  20299  decpmatmulsumfsupp  20559  pmatcollpw1lem1  20560  pmatcollpw2lem  20563  pm2mpmhmlem1  20604  cpmidpmatlem3  20658  cpmidgsum2  20665  tgcl  20754  neiss  20894  ssnei2  20901  tgcnp  21038  cnpco  21052  cnpresti  21073  lmcnp  21089  hausnei2  21138  1stcrest  21237  nlly2i  21260  llyss  21263  nllyss  21264  reftr  21298  lfinun  21309  txcnpi  21392  txcmplem1  21425  tx1stc  21434  nrmr0reg  21533  fbssfi  21622  fbfinnfr  21626  fgcl  21663  ufinffr  21714  elfm2  21733  fmfnfmlem1  21739  fmco  21746  fbflim2  21762  flffbas  21780  flftg  21781  cnpflf2  21785  alexsubALT  21836  cnextcn  21852  isucn2  22064  ucnima  22066  blssexps  22212  blssex  22213  mopni3  22280  neibl  22287  metss  22294  metcnp3  22326  cfilucfil  22345  metustbl  22352  psmetutop  22353  rescncf  22681  lebnum  22744  xlebnum  22745  lebnumii  22746  lmmbr  23037  fgcfil  23050  ovolsslem  23233  ovolunlem1  23246  ovoliunnul  23256  itgcn  23590  ellimc3  23624  c1lip3  23743  itgsubstlem  23792  plyss  23936  ulmclm  24122  ulmcau  24130  ulmcn  24134  rlimcxp  24681  chtppilimlem2  25144  chtppilim  25145  midex  25610  umgrnloop0  25985  usgrnloop0ALT  26078  uhgr2edg  26081  vtxduhgr0nedg  26369  wlkonl1iedg  26542  elwspths2on  26834  3cyclfrgrrn2  27131  frgrwopreg1  27160  frgrwopreg2  27161  isgrpo  27321  tpr2rico  29932  esumpcvgval  30114  omssubadd  30336  connpconn  31191  cvmliftlem15  31254  cvmlift2lem10  31268  fnessref  32327  ptrecube  33380  poimirlem29  33409  poimirlem30  33410  poimirlem31  33411  fdc1  33513  sstotbnd3  33546  totbndss  33547  heibor1lem  33579  heibor1  33580  opidonOLD  33622  rngmgmbs4  33701  lvoli2  34686  paddss2  34923  lhpexle1lem  35112  lhpexle2lem  35114  dvhdimlem  36552  dvh3dim3N  36557  mapdh9a  36898  hdmap11lem2  36953  fiphp3d  37202  pell1qrss14  37251  eliuniin  39099  restuni3  39121  eliuniin2  39123  disjrnmpt2  39191  rnmptbd2lem  39279  ssfiunibd  39336  supminfxrrnmpt  39514  climrec  39635  islptre  39651  lptre2pt  39672  limsupmnfuzlem  39758  limsupre3lem  39764  limsupvaluz2  39770  supcnvlimsup  39772  liminfvalxr  39809  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  stoweidlem27  40007  stoweidlem29  40009  stoweidlem35  40015  stoweidlem48  40028  stoweidlem62  40042  fourierdlem48  40134  fourierdlem64  40150  fourierdlem65  40151  fourierdlem71  40157  fourierdlem73  40159  fourierdlem94  40180  fourierdlem103  40189  fourierdlem104  40190  fourierdlem112  40198  fourierdlem113  40199  sge0isum  40407  sge0seq  40426  meaiuninclem  40460  carageniuncllem2  40499  ovnsslelem  40537  hoidmvlelem1  40572  afvelima  41010  sgoldbeven3prm  41436  nnsum4primes4  41442  nnsum4primesprm  41444  nnsum4primesgbe  41446  nnsum4primesle9  41448  pgrpgt2nabl  41912
  Copyright terms: Public domain W3C validator