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

Theorem simprbi 500
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simprbi.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
simprbi (𝜑𝜒)

Proof of Theorem simprbi
StepHypRef Expression
1 simprbi.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21biimpi 219 . 2 (𝜑 → (𝜓𝜒))
32simprd 499 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-an 400
This theorem is referenced by:  simplbiim  508  xornan  1511  sb1ALT  2558  eumo  2638  reurmo  3378  pssne  4024  pssn2lp  4029  ssnpss  4031  eldifn  4055  elinel2  4123  rabsnt  4627  eldifsni  4683  unimax  4836  ssintub  4856  moop2  5357  pwssun  5421  weso  5510  opelxp2  5561  wfisg  6151  ordwe  6172  funmo  6340  funopg  6358  funun  6370  fununi  6399  fndm  6425  frn  6493  f1ss  6555  f1ssr  6556  forn  6568  f1f1orn  6601  f1orescnv  6605  f1imacnv  6606  funcocnv2  6614  dffv2  6733  exfo  6848  foelrn  6849  isorel  7058  isoini2  7071  f1ofveu  7130  fovcl  7258  onminesb  7493  onminsb  7494  tfis  7549  limomss  7565  nnlim  7573  ssnlim  7579  curry1  7782  curry2  7785  f1o2ndf1  7801  fnwelem  7808  mpoxopn0yelv  7862  wfrlem5  7942  tz7.48lem  8060  dif20el  8113  oeordi  8196  oeeulem  8210  oeeui  8211  nnawordex  8246  swoer  8302  eceqoveq  8385  mapsnconst  8439  resixpfo  8483  boxcutc  8488  sdomnen  8521  en0  8555  en1  8559  fodomr  8652  unxpdomlem3  8708  fineqvlem  8716  f1opwfi  8812  fsuppcolem  8848  fsuppco  8849  mapfienlem1  8852  mapfienlem2  8853  supub  8907  suplub  8908  ordtypelem2  8967  ordtypelem3  8968  ordtypelem6  8971  ordtypelem7  8972  wemapso2lem  9000  wdom2d  9028  brwdom3  9030  ixpiunwdom  9038  inf3lem2  9076  inf3lem6  9080  oancom  9098  infdifsn  9104  cantnfp1lem3  9127  cantnflem3  9138  cantnflem4  9139  oef1o  9145  cnfcom3  9151  tctr  9166  tz9.12lem3  9202  scottex  9298  cardid2  9366  infxpenlem  9424  acni3  9458  cardaleph  9500  iscard3  9504  dfac5lem4  9537  dfac5lem5  9538  kmlem1  9561  cofsmo  9680  fin4en1  9720  enfin2i  9732  fin23lem28  9751  fin23lem38  9760  isf32lem6  9769  enfin1ai  9795  hsmexlem2  9838  hsmexlem4  9840  domtriomlem  9853  axdc2lem  9859  axdc3lem2  9862  ac6num  9890  zorn2lem2  9908  brdom3  9939  alephval2  9983  alephreg  9993  pwcfsdom  9994  smobeth  9997  fpwwe2lem6  10046  fpwwe2lem13  10053  canthp1lem2  10064  pwfseqlem3  10071  hargch  10084  winalim2  10107  gchina  10110  inar1  10186  0npi  10293  mulclpi  10304  mulcanpi  10311  nlt1pi  10317  nqereu  10340  prcdnq  10404  prnmax  10406  ltresr2  10552  axrnegex  10573  axpre-sup  10580  eluz2gt1  12308  1nuz2  12312  zsupss  12325  rpgt0  12389  ixxss1  12744  ixxss2  12745  ixxss12  12746  lbioo  12757  ubioo  12758  iccss2  12796  iccssico2  12799  elfzuz3  12899  serge0  13420  expge0  13461  expge1  13462  expaddzlem  13468  hashrabsn1  13731  hashfun  13794  cshinj  14164  relexpuzrel  14403  shftfn  14424  sqrlem6  14599  rlimss  14851  lo1dm  14868  o1dm  14879  rlimrege0  14928  fsumf1o  15072  fsumge0  15142  incexc2  15185  supcvg  15203  fprodf1o  15292  divalglem9  15742  bitsfzolem  15773  bitsf1  15785  gcdcllem1  15838  bezout  15881  nprm  16022  dvdsprm  16037  coprm  16045  dfphi2  16101  phimullem  16106  phisum  16117  expnprm  16228  prmreclem2  16243  prmreclem5  16246  1arith  16253  4sqlem18  16288  vdwnnlem3  16323  ramtlecl  16326  rami  16341  0ram  16346  ramub1lem1  16352  prmgaplem5  16381  acsfiel  16917  isacs1i  16920  catlid  16946  catrid  16947  fullfo  17174  fthf1  17179  fthoppc  17185  invfuc  17236  prslem  17533  posi  17552  dlatmjdi  17796  pslem  17808  tsrlin  17821  cnvtsr  17824  tsrdir  17840  mndid  17913  mhmf  17953  mhmlin  17955  mhm0  17956  mndind  17984  grpinvex  18105  grplinv  18144  mulgz  18247  mulgdirlem  18250  mulgdir  18251  mulgass  18256  nsgbi  18301  nmzbi  18308  ghmf  18354  ghmlin  18355  conjnsg  18386  gimf1o  18395  gagrpid  18416  gaf  18417  gaass  18419  psgnunilem5  18614  odid  18658  odf1o2  18690  gexid  18698  sylow1lem4  18718  pj1id  18817  efgredeu  18870  ablcmn  18905  cmncom  18915  mulgdi  18940  torsubg  18967  cyggenod2  18997  cygctb  19005  ghmcyg  19009  dprdf1o  19147  ablfacrplem  19180  ablfaclem2  19201  ablfac2  19204  simpg2nsg  19211  fincygsubgodexd  19228  crngmgp  19298  rhmmhm  19470  rhmghm  19473  drngunit  19500  drngmgp  19507  drngid  19509  subrgss  19529  subrg1cl  19536  issubdrg  19553  cntzsdrg  19574  abvge0  19589  srngcnv  19617  lmhmlin  19800  lmimf1o  19828  lvecdrng  19870  lspsolvlem  19907  islbs3  19920  lbsextlem3  19925  2idlcpbl  20000  nzrnz  20026  opprnzr  20031  rrgeq0i  20055  domneq0  20063  domnrrg  20066  drngdomn  20069  fldidom  20071  zringunit  20181  prmirredlem  20186  znidomb  20253  cygzn  20262  psgndiflemB  20289  pjf  20402  frlmsslsp  20485  frlmlbs  20486  f1lindf  20511  assalem  20546  mplsubrglem  20677  mplcoe1  20705  mplbas2  20710  opsrtoslem2  20724  mplelsfi  20730  coe1mul2  20898  pmatcoe1fsupp  21306  toponuni  21519  tpsuni  21541  mretopd  21697  neips  21718  neiptoptop  21736  neiptopnei  21737  perflp  21759  perfi  21760  cnf  21851  cnpf  21852  cnpimaex  21861  cnima  21870  t0sep  21929  t1ficld  21932  hausnei  21933  pnrmcld  21947  cnrmi  21965  cmpcov  21994  tgcmp  22006  hauscmplem  22011  connclo  22020  1stcclb  22049  2ndcdisj  22061  llyi  22079  nllyi  22080  ptpjpre1  22176  ptpjcn  22216  ptpjopn  22217  ptclsg  22220  dfac14  22223  txdis1cn  22240  pthaus  22243  hauseqlcld  22251  txkgen  22257  xkococn  22265  txconn  22294  hmeocnvcn  22366  fbssfi  22442  filss  22458  uffixfr  22528  flimneiss  22571  flimelbas  22573  flimfnfcls  22633  alexsubb  22651  alexsubALT  22656  ptcmplem2  22658  ptcmplem3  22659  ptcmplem4  22660  tmdgsum2  22701  ghmcnp  22720  tgpt0  22724  qustgplem  22726  istdrg2  22783  vscacn  22791  tvctdrg  22798  uspreg  22880  ucncn  22891  neipcfilu  22902  cuspcvg  22907  psmetxrge0  22920  isxmet2d  22934  prdsxmetlem  22975  imasdsf1olem  22980  xmstopn  23058  mstopn  23059  stdbdxmet  23122  prdsxmslem2  23136  nrgabv  23267  nmvs  23282  nvclvec  23303  nmoge0  23327  nghmcl  23333  nmoi  23334  nghmghm  23340  nmhmlmhm  23355  nmhmnghm  23356  icccmp  23430  xrge0gsumle  23438  metds0  23455  metdstri  23456  metdsre  23458  metdseq0  23459  metdscnlem  23460  metnrmlem1a  23463  icopnfcnv  23547  xrhmeo  23551  pcoval1  23618  cvslvec  23730  cvsunit  23736  cphreccllem  23783  cphsscph  23855  cmetcvg  23889  lmle  23905  cmscmet  23950  cmetcusp1  23957  hlcph  23968  minveclem4  24036  ivthlem3  24057  ovolmge0  24081  ovolicc1  24120  ovolicc2lem3  24123  ovolicc2lem5  24125  dyadmbl  24204  i1ff  24280  i1frn  24281  i1fima2  24283  itg2monolem1  24354  dvnres  24534  c1liplem1  24599  c1lip2  24601  dvge0  24609  lhop1lem  24616  itgsubstlem  24651  fta1glem2  24767  fta1b  24770  plyf  24795  plypf1  24809  plyadd  24814  plymul  24815  coeeu  24822  dgrlem  24826  coeid  24835  elqaalem3  24917  aareccl  24922  eff1olem  25140  relogf1o  25158  logdmn0  25231  logcnlem2  25234  logcnlem3  25235  efopnlem1  25247  efopnlem2  25248  logtayl2  25253  cxpcn3lem  25336  cxpcn3  25337  logbgcd1irr  25380  atandmneg  25492  atandmcj  25495  efiatan2  25503  cosatan  25507  cosatanne0  25508  dvatan  25521  areage0  25549  cxp2lim  25562  jensenlem2  25573  jensen  25574  eldmgm  25607  dmgmaddn0  25608  dmlogdmgm  25609  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem5  25618  lgambdd  25622  lgamucov  25623  ftalem3  25660  efnnfsumcl  25688  efchtdvds  25744  sqff1o  25767  fsumdvdsdiaglem  25768  dvdsppwf1o  25771  dvdsflf1o  25772  musum  25776  muinv  25778  dvdsmulf1o  25779  lgsfle1  25890  lgsle1  25896  lgsdirprm  25915  lgsne0  25919  lgseisenlem3  25961  lgseisenlem4  25962  lgsquadlem1  25964  lgsquadlem2  25965  chebbnd1  26056  chtppilim  26059  chpchtlim  26063  chpo1ub  26064  dchrmusumlema  26077  dchrvmasumlem1  26079  dchrisum0lema  26098  dchrisum0lem2a  26101  logsqvma  26126  selberg3lem2  26142  pntrsumo1  26149  pnt2  26197  ostthlem1  26211  ostth3  26222  axtgcgrrflx  26256  axtgcgrid  26257  axtgsegcon  26258  axtg5seg  26259  axtgbtwnid  26260  axtgpasch  26261  axtgcont1  26262  tglng  26340  axcontlem7  26764  axcontlem10  26767  upgrle  26883  umgredg2  26893  lfgredgge2  26917  usgredg2ALT  26983  usgr1vr  27045  usgrexmpledg  27052  upgrres1  27103  fusgrvtxfi  27109  vtxnbuvtx  27181  cusgrcplgr  27210  vdumgr0  27270  vtxdgoddnumeven  27343  trlres  27490  usgr2pth  27553  cyclispthon  27590  clwwlknlen  27817  clwwnonrepclwwnon  28130  2clwwlk2  28133  ablocom  28331  phpar2  28606  cbncms  28648  hlph  28672  hcaucvg  28969  hlimconvi  28974  shaddcl  29000  shmulcl  29001  chlimi  29017  chcompl  29025  choc1  29110  nmopre  29653  cnopc  29696  lnopl  29697  unop  29698  hmop  29705  cnfnc  29713  lnfnl  29714  nlelshi  29843  cnlnadjlem5  29854  elpjidm  29967  mdslle1i  30100  mdslle2i  30101  atcv0  30125  chpssati  30146  fovcld  30399  aciunf1lem  30425  padct  30481  ssnnssfz  30536  ccatf1  30651  swrdrndisj  30657  ressprs  30668  oduprs  30669  resspos  30672  resstos  30673  tleile  30674  pwrssmgc  30706  ogrpinv0le  30766  ogrpsub  30767  ogrpaddlt  30768  cyc3evpm  30842  cycpmgcl  30845  cycpmconjslem2  30847  cyc3conja  30849  isarchi3  30866  archirng  30867  archirngz  30868  archiabllem1a  30870  archiabllem1b  30871  archiabllem2a  30873  archiabllem2c  30874  archiabllem2b  30875  archiabl  30877  orngsqr  30928  ornglmulle  30929  orngrmulle  30930  ofldtos  30935  ofldlt1  30937  ofldchr  30938  suborng  30939  subofld  30940  isarchiofld  30941  nn0omnd  30965  prmidl0  31034  qsidomlem1  31036  krull  31051  sradrng  31076  extdg1id  31141  madjusmdetlem4  31183  qtophaus  31189  crefi  31200  cmpcref  31203  cmppcmp  31211  pcmplfin  31213  zart0  31232  tpr2rico  31265  rge0scvg  31302  zrhunitpreima  31329  qqhrhm  31340  esummono  31423  gsumesum  31428  esumrnmpt2  31437  esumpinfval  31442  esumpcvgval  31447  esumpmono  31448  0elsiga  31483  sigaclcu  31486  issgon  31492  inelpisys  31523  ldsysgenld  31529  ldgenpisyslem1  31532  sxuni  31562  isrnmeas  31569  measvuni  31583  measssd  31584  ddemeas  31605  imambfm  31630  elmbfmvol2  31635  dya2icoseg2  31646  omssubaddlem  31667  omssubadd  31668  carsgsigalem  31683  pmeasmono  31692  sibfinima  31707  oddpwdc  31722  oddpwdcv  31723  eulerpartlemf  31738  eulerpartlemt  31739  eulerpartlemr  31742  eulerpartlemgvv  31744  eulerpartlemgs2  31748  fiblem  31766  probtot  31780  ballotlem4  31866  ballotlem5  31867  ballotlemfrc  31894  ballotlemirc  31899  ballotth  31905  hgt750lemb  32037  bnj642  32129  bnj643  32130  bnj645  32131  bnj707  32136  bnj1379  32212  bnj1538  32237  bnj110  32240  bnj93  32245  bnj906  32312  bnj1006  32342  bnj1110  32364  bnj1121  32367  bnj1204  32394  bnj1321  32409  bnj1364  32410  bnj1398  32416  bnj1450  32432  bnj1312  32440  bnj1501  32449  bnj1523  32453  0nn0m1nnn0  32461  subfacp1lem3  32539  subfacp1lem5  32541  pconncn  32581  connpconn  32592  cvmcov  32620  cvmliftlem1  32642  cvmliftlem10  32651  cvmlift2lem11  32670  cvmlift2lem12  32671  msubff1  32913  mvhf1  32916  mthmpps  32939  mclspps  32941  fundmpss  33119  tfisg  33165  frpoinsg  33191  frinsg  33197  sltval2  33273  funpartfun  33514  fnetg  33803  neibastop1  33817  filnetlem3  33838  onint1  33907  bj-nnfa  34172  bj-idres  34572  bj-rvecrr  34708  icorempo  34765  pibt2  34831  wl-nfeqfb  34938  phpreu  35038  fin2solem  35040  fin2so  35041  lindsenlbs  35049  matunitlindflem1  35050  matunitlindflem2  35051  matunitlindf  35052  ptrest  35053  poimirlem1  35055  poimirlem2  35056  poimirlem3  35057  poimirlem4  35058  poimirlem5  35059  poimirlem6  35060  poimirlem7  35061  poimirlem8  35062  poimirlem9  35063  poimirlem10  35064  poimirlem11  35065  poimirlem12  35066  poimirlem13  35067  poimirlem14  35068  poimirlem15  35069  poimirlem16  35070  poimirlem17  35071  poimirlem18  35072  poimirlem19  35073  poimirlem20  35074  poimirlem21  35075  poimirlem22  35076  poimirlem23  35077  poimirlem24  35078  poimirlem26  35080  poimirlem27  35081  poimirlem29  35083  poimirlem31  35085  mblfinlem2  35092  dvtan  35104  itg2gt0cn  35109  ftc1anclem7  35133  ftc1anclem8  35134  ftc1anc  35135  cover2  35149  indexa  35168  istotbnd3  35206  sstotbnd2  35209  sstotbnd  35210  totbndss  35212  equivtotbnd  35213  isbnd3  35219  totbndbnd  35224  equivbnd  35225  prdsbnd  35228  prdstotbnd  35229  heibor  35256  zrdivrng  35388  crngocom  35436  isfld2  35440  dmncrng  35491  eqvrelrel  35989  disjrel  36120  prter2  36174  toycom  36266  lsateln0  36288  lpssat  36306  lssat  36309  oposlem  36475  olop  36507  omllaw  36536  cvlexch1  36621  dihpN  38629  mapdordlem2  38930  prjspertr  39594  nacsfg  39641  nacsfix  39648  mzpindd  39682  diophrw  39695  diophrex  39711  rexzrexnn0  39740  pell1234qrdich  39797  rmspecnonsq  39843  rmspecfund  39845  rmspecpos  39852  monotoddzzfi  39878  ltrmxnn0  39885  rmxnn  39887  jm2.23  39932  jm3.1lem2  39954  dnnumch3  39986  lnmlssfg  40019  lnmlmic  40027  lnrlnm  40052  lnr2i  40055  lpirlnr  40056  hbtlem6  40068  hbt  40069  mnccoe  40077  idomrootle  40134  proot1mul  40138  proot1hash  40139  deg1mhm  40146  ntrneifv2  40778  grucollcld  40963  mnurndlem1  40984  radcnvrat  41013  binomcxplemdvbinom  41052  binomcxplemcvg  41053  binomcxplemnotnn0  41055  ordelordALT  41238  2uasbanh  41262  ordelordALTVD  41568  elixpconstg  41720  rabidim2  41733  foelrnf  41808  disjinfi  41815  supminfxr2  42103  sumnnodd  42267  stoweidlem7  42644  stoweidlem14  42651  stoweidlem16  42653  stoweidlem24  42661  stoweidlem31  42668  stoweidlem54  42691  wallispilem3  42704  fourierdlem42  42786  fourierdlem48  42791  fourierdlem51  42794  fourierdlem64  42807  fourierdlem76  42819  fourierdlem79  42822  fourierdlem81  42824  fourierdlem87  42830  etransclem28  42899  etransclem32  42903  sge0fodjrnlem  43050  hoidmvlelem3  43231  pimrecltpos  43339  pimrecltneg  43353  issmflem  43356  smfaddlem1  43391  smfsuplem1  43437  smfsuplem3  43439  smflimsuplem7  43452  smfliminflem  43456  nfunsnafv  43693  faovcl  43751  tz6.12-2-afv2  43788  tz6.12i-afv2  43794  sprel  43996  evendiv2z  44145  oddp1div2z  44146  2dvdseven  44166  2ndvdsodd  44168  perfectALTVlem1  44234  sbgoldbm  44297  clintopcllaw  44466  0ringbas  44490  rnghmmgmhm  44513  uzlidlring  44548  rnghmsubcsetclem1  44594  rngccatidALTV  44608  zrinitorngc  44619  zrtermorngc  44620  rhmsubcsetclem1  44640  funcringcsetcALTV2lem7  44661  ringccatidALTV  44671  funcringcsetclem7ALTV  44684  irinitoringc  44688  zrtermoringc  44689  fldhmsubc  44703  fldhmsubcALTV  44721  ssnn0ssfz  44746  el0ldepsnzr  44871  regt1loggt0  44945  elbigodm  44964  fllogbd  44969  rrx2xpref1o  45127  elsetrecslem  45223
  Copyright terms: Public domain W3C validator