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

Theorem simprbi 497
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 217 . 2 (𝜑 → (𝜓𝜒))
32simprd 496 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  simplbiim  505  xornan  1503  sb1ALT  2578  eumo  2659  reurmo  3434  pssne  4072  pssn2lp  4077  ssnpss  4079  eldifn  4103  elinel2  4172  rabsnt  4661  eldifsni  4716  unimax  4867  ssintub  4887  moop2  5384  pwssun  5449  weso  5540  opelxp2  5591  wfisg  6177  ordwe  6198  funmo  6365  funopg  6383  funun  6394  fununi  6423  fndm  6449  frn  6514  f1ss  6574  f1ssr  6575  forn  6587  f1f1orn  6620  f1orescnv  6624  f1imacnv  6625  funcocnv2  6633  dffv2  6750  exfo  6864  foelrn  6865  isorel  7068  isoini2  7081  f1ofveu  7140  fovcl  7268  onminesb  7501  onminsb  7502  tfis  7557  limomss  7573  nnlim  7581  ssnlim  7587  curry1  7790  curry2  7793  f1o2ndf1  7809  fnwelem  7816  mpoxopn0yelv  7870  wfrlem5  7950  tz7.48lem  8068  dif20el  8121  oeordi  8203  oeeulem  8217  oeeui  8218  nnawordex  8253  swoer  8309  eceqoveq  8392  mapsnconst  8445  resixpfo  8489  boxcutc  8494  sdomnen  8527  en0  8561  en1  8565  fodomr  8657  unxpdomlem3  8713  fineqvlem  8721  f1opwfi  8817  fsuppcolem  8853  fsuppco  8854  mapfienlem1  8857  mapfienlem2  8858  supub  8912  suplub  8913  ordtypelem2  8972  ordtypelem3  8973  ordtypelem6  8976  ordtypelem7  8977  wemapso2lem  9005  wdom2d  9033  brwdom3  9035  ixpiunwdom  9044  inf3lem2  9081  inf3lem6  9085  oancom  9103  infdifsn  9109  cantnfp1lem3  9132  cantnflem3  9143  cantnflem4  9144  oef1o  9150  cnfcom3  9156  tctr  9171  tz9.12lem3  9207  scottex  9303  cardid2  9371  infxpenlem  9428  acni3  9462  cardaleph  9504  iscard3  9508  dfac5lem4  9541  dfac5lem5  9542  kmlem1  9565  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  12309  1nuz2  12313  zsupss  12326  rpgt0  12391  ixxss1  12746  ixxss2  12747  ixxss12  12748  lbioo  12759  ubioo  12760  iccss2  12797  iccssico2  12800  elfzuz3  12895  serge0  13414  expge0  13455  expge1  13456  expaddzlem  13462  hashrabsn1  13725  hashfun  13788  cshinj  14163  relexpuzrel  14401  shftfn  14422  sqrlem6  14597  rlimss  14849  lo1dm  14866  o1dm  14877  rlimrege0  14926  fsumf1o  15070  fsumge0  15140  incexc2  15183  supcvg  15201  fprodf1o  15290  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  16915  isacs1i  16918  catlid  16944  catrid  16945  fullfo  17172  fthf1  17177  fthoppc  17183  invfuc  17234  prslem  17531  posi  17550  dlatmjdi  17794  pslem  17806  tsrlin  17819  cnvtsr  17822  tsrdir  17838  mndid  17911  mhmf  17951  mhmlin  17953  mhm0  17954  mndind  17982  grpinvex  18053  grplinv  18092  mulgz  18195  mulgdirlem  18198  mulgdir  18199  mulgass  18204  nsgbi  18249  nmzbi  18256  ghmf  18302  ghmlin  18303  conjnsg  18334  gimf1o  18343  gagrpid  18364  gaf  18365  gaass  18367  psgnunilem5  18553  odid  18597  odf1o2  18629  gexid  18637  sylow1lem4  18657  pj1id  18756  efgredeu  18809  ablcmn  18844  cmncom  18854  mulgdi  18878  torsubg  18905  cyggenod2  18935  cygctb  18943  ghmcyg  18947  dprdf1o  19085  ablfacrplem  19118  ablfaclem2  19139  ablfac2  19142  simpg2nsg  19149  fincygsubgodexd  19166  crngmgp  19236  rhmmhm  19405  rhmghm  19408  drngunit  19438  drngmgp  19445  drngid  19447  subrgss  19467  subrg1cl  19474  issubdrg  19491  cntzsdrg  19512  abvge0  19527  srngcnv  19555  lmhmlin  19738  lmimf1o  19766  lvecdrng  19808  lspsolvlem  19845  islbs3  19858  lbsextlem3  19863  2idlcpbl  19937  nzrnz  19963  opprnzr  19968  rrgeq0i  19992  domneq0  20000  domnrrg  20003  drngdomn  20006  fldidom  20008  assalem  20019  mplsubrglem  20149  mplcoe1  20176  mplbas2  20181  opsrtoslem2  20195  mplelsfi  20201  coe1mul2  20367  zringunit  20565  prmirredlem  20570  znidomb  20638  cygzn  20647  psgndiflemB  20674  pjf  20787  frlmsslsp  20870  frlmlbs  20871  f1lindf  20896  pmatcoe1fsupp  21239  toponuni  21452  tpsuni  21474  mretopd  21630  neips  21651  neiptoptop  21669  neiptopnei  21670  perflp  21692  perfi  21693  cnf  21784  cnpf  21785  cnpimaex  21794  cnima  21803  t0sep  21862  t1ficld  21865  hausnei  21866  pnrmcld  21880  cnrmi  21898  cmpcov  21927  tgcmp  21939  hauscmplem  21944  connclo  21953  1stcclb  21982  2ndcdisj  21994  llyi  22012  nllyi  22013  ptpjpre1  22109  ptpjcn  22149  ptpjopn  22150  ptclsg  22153  dfac14  22156  txdis1cn  22173  pthaus  22176  hauseqlcld  22184  txkgen  22190  xkococn  22198  txconn  22227  hmeocnvcn  22299  fbssfi  22375  filss  22391  uffixfr  22461  flimneiss  22504  flimelbas  22506  flimfnfcls  22566  alexsubb  22584  alexsubALT  22589  ptcmplem2  22591  ptcmplem3  22592  ptcmplem4  22593  tmdgsum2  22634  ghmcnp  22652  tgpt0  22656  qustgplem  22658  istdrg2  22715  vscacn  22723  tvctdrg  22730  uspreg  22812  ucncn  22823  neipcfilu  22834  cuspcvg  22839  psmetxrge0  22852  isxmet2d  22866  prdsxmetlem  22907  imasdsf1olem  22912  xmstopn  22990  mstopn  22991  stdbdxmet  23054  prdsxmslem2  23068  nrgabv  23199  nmvs  23214  nvclvec  23235  nmoge0  23259  nghmcl  23265  nmoi  23266  nghmghm  23272  nmhmlmhm  23287  nmhmnghm  23288  icccmp  23362  xrge0gsumle  23370  metds0  23387  metdstri  23388  metdsre  23390  metdseq0  23391  metdscnlem  23392  metnrmlem1a  23395  icopnfcnv  23475  xrhmeo  23479  pcoval1  23546  cvslvec  23658  cvsunit  23664  cphreccllem  23711  cphsscph  23783  cmetcvg  23817  lmle  23833  cmscmet  23878  cmetcusp1  23885  hlcph  23896  minveclem4  23964  ivthlem3  23983  ovolmge0  24007  ovolicc1  24046  ovolicc2lem3  24049  ovolicc2lem5  24051  dyadmbl  24130  i1ff  24206  i1frn  24207  i1fima2  24209  itg2monolem1  24280  dvnres  24457  c1liplem1  24522  c1lip2  24524  dvge0  24532  lhop1lem  24539  itgsubstlem  24574  fta1glem2  24689  fta1b  24692  plyf  24717  plypf1  24731  plyadd  24736  plymul  24737  coeeu  24744  dgrlem  24748  coeid  24757  elqaalem3  24839  aareccl  24844  eff1olem  25059  relogf1o  25077  logdmn0  25150  logcnlem2  25153  logcnlem3  25154  efopnlem1  25166  efopnlem2  25167  logtayl2  25172  cxpcn3lem  25255  cxpcn3  25256  logbgcd1irr  25299  atandmneg  25411  atandmcj  25414  efiatan2  25422  cosatan  25426  cosatanne0  25427  dvatan  25440  areage0  25469  cxp2lim  25482  jensenlem2  25493  jensen  25494  eldmgm  25527  dmgmaddn0  25528  dmlogdmgm  25529  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem5  25538  lgambdd  25542  lgamucov  25543  ftalem3  25580  efnnfsumcl  25608  efchtdvds  25664  sqff1o  25687  fsumdvdsdiaglem  25688  dvdsppwf1o  25691  dvdsflf1o  25692  musum  25696  muinv  25698  dvdsmulf1o  25699  lgsfle1  25810  lgsle1  25816  lgsdirprm  25835  lgsne0  25839  lgseisenlem3  25881  lgseisenlem4  25882  lgsquadlem1  25884  lgsquadlem2  25885  chebbnd1  25976  chtppilim  25979  chpchtlim  25983  chpo1ub  25984  dchrmusumlema  25997  dchrvmasumlem1  25999  dchrisum0lema  26018  dchrisum0lem2a  26021  logsqvma  26046  selberg3lem2  26062  pntrsumo1  26069  pnt2  26117  ostthlem1  26131  ostth3  26142  axtgcgrrflx  26176  axtgcgrid  26177  axtgsegcon  26178  axtg5seg  26179  axtgbtwnid  26180  axtgpasch  26181  axtgcont1  26182  tglng  26260  axcontlem7  26684  axcontlem10  26687  upgrle  26803  umgredg2  26813  lfgredgge2  26837  usgredg2ALT  26903  usgr1vr  26965  usgrexmpledg  26972  upgrres1  27023  fusgrvtxfi  27029  vtxnbuvtx  27101  cusgrcplgr  27130  vdumgr0  27190  vtxdgoddnumeven  27263  trlres  27410  usgr2pth  27473  cyclispthon  27510  clwwlknlen  27738  clwwnonrepclwwnon  28052  2clwwlk2  28055  ablocom  28253  phpar2  28528  cbncms  28570  hlph  28594  hcaucvg  28891  hlimconvi  28896  shaddcl  28922  shmulcl  28923  chlimi  28939  chcompl  28947  choc1  29032  nmopre  29575  cnopc  29618  lnopl  29619  unop  29620  hmop  29627  cnfnc  29635  lnfnl  29636  nlelshi  29765  cnlnadjlem5  29776  elpjidm  29889  mdslle1i  30022  mdslle2i  30023  atcv0  30047  chpssati  30068  fovcld  30314  aciunf1lem  30336  padct  30382  ssnnssfz  30437  ccatf1  30553  swrdrndisj  30559  ressprs  30570  oduprs  30571  resspos  30574  resstos  30575  tleile  30576  ogrpinv0le  30644  ogrpsub  30645  ogrpaddlt  30646  cyc3evpm  30720  cycpmgcl  30723  cycpmconjslem2  30725  cyc3conja  30727  isarchi3  30744  archirng  30745  archirngz  30746  archiabllem1a  30748  archiabllem1b  30749  archiabllem2a  30751  archiabllem2c  30752  archiabllem2b  30753  archiabl  30755  orngsqr  30805  ornglmulle  30806  orngrmulle  30807  ofldtos  30812  ofldlt1  30814  ofldchr  30815  suborng  30816  subofld  30817  isarchiofld  30818  nn0omnd  30842  qsidomlem1  30883  sradrng  30888  extdg1id  30953  madjusmdetlem4  30995  qtophaus  31000  crefi  31011  cmpcref  31014  cmppcmp  31022  pcmplfin  31024  tpr2rico  31055  rge0scvg  31092  zrhunitpreima  31119  qqhrhm  31130  esummono  31213  gsumesum  31218  esumrnmpt2  31227  esumpinfval  31232  esumpcvgval  31237  esumpmono  31238  0elsiga  31273  sigaclcu  31276  issgon  31282  inelpisys  31313  ldsysgenld  31319  ldgenpisyslem1  31322  sxuni  31352  isrnmeas  31359  measvuni  31373  measssd  31374  ddemeas  31395  imambfm  31420  elmbfmvol2  31425  dya2icoseg2  31436  omssubaddlem  31457  omssubadd  31458  carsgsigalem  31473  pmeasmono  31482  sibfinima  31497  oddpwdc  31512  oddpwdcv  31513  eulerpartlemf  31528  eulerpartlemt  31529  eulerpartlemr  31532  eulerpartlemgvv  31534  eulerpartlemgs2  31538  fiblem  31556  probtot  31570  ballotlem4  31656  ballotlem5  31657  ballotlemfrc  31684  ballotlemirc  31689  ballotth  31695  hgt750lemb  31827  bnj642  31919  bnj643  31920  bnj645  31921  bnj707  31926  bnj1379  32002  bnj1538  32027  bnj110  32030  bnj93  32035  bnj906  32102  bnj1006  32131  bnj1110  32152  bnj1121  32155  bnj1204  32182  bnj1321  32197  bnj1364  32198  bnj1398  32204  bnj1450  32220  bnj1312  32228  bnj1501  32237  bnj1523  32241  0nn0m1nnn0  32249  subfacp1lem3  32327  subfacp1lem5  32329  pconncn  32369  connpconn  32380  cvmcov  32408  cvmliftlem1  32430  cvmliftlem10  32439  cvmlift2lem11  32458  cvmlift2lem12  32459  msubff1  32701  mvhf1  32704  mthmpps  32727  mclspps  32729  fundmpss  32907  tfisg  32953  frpoinsg  32979  frinsg  32985  sltval2  33061  funpartfun  33302  fnetg  33591  neibastop1  33605  filnetlem3  33626  onint1  33695  bj-nnfa  33958  bj-idres  34345  bj-rvecrr  34467  icorempo  34515  pibt2  34581  wl-nfeqfb  34658  phpreu  34758  fin2solem  34760  fin2so  34761  lindsenlbs  34769  matunitlindflem1  34770  matunitlindflem2  34771  matunitlindf  34772  ptrest  34773  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem5  34779  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem9  34783  poimirlem10  34784  poimirlem11  34785  poimirlem12  34786  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  poimirlem21  34795  poimirlem22  34796  poimirlem23  34797  poimirlem24  34798  poimirlem26  34800  poimirlem27  34801  poimirlem29  34803  poimirlem31  34805  mblfinlem2  34812  dvtan  34824  itg2gt0cn  34829  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  cover2  34872  indexa  34891  istotbnd3  34932  sstotbnd2  34935  sstotbnd  34936  totbndss  34938  equivtotbnd  34939  isbnd3  34945  totbndbnd  34950  equivbnd  34951  prdsbnd  34954  prdstotbnd  34955  heibor  34982  zrdivrng  35114  crngocom  35162  isfld2  35166  dmncrng  35217  eqvrelrel  35714  disjrel  35845  prter2  35899  toycom  35991  lsateln0  36013  lpssat  36031  lssat  36034  oposlem  36200  olop  36232  omllaw  36261  cvlexch1  36346  dihpN  38354  mapdordlem2  38655  prjspertr  39135  nacsfg  39182  nacsfix  39189  mzpindd  39223  diophrw  39236  diophrex  39252  rexzrexnn0  39281  pell1234qrdich  39338  rmspecnonsq  39384  rmspecfund  39386  rmspecpos  39393  monotoddzzfi  39419  ltrmxnn0  39426  rmxnn  39428  jm2.23  39473  jm3.1lem2  39495  dnnumch3  39527  lnmlssfg  39560  lnmlmic  39568  lnrlnm  39593  lnr2i  39596  lpirlnr  39597  hbtlem6  39609  hbt  39610  mnccoe  39618  idomrootle  39675  proot1mul  39679  proot1hash  39680  deg1mhm  39687  ntrneifv2  40310  grucollcld  40476  mnurndlem1  40497  radcnvrat  40526  binomcxplemdvbinom  40565  binomcxplemcvg  40566  binomcxplemnotnn0  40568  ordelordALT  40751  2uasbanh  40775  ordelordALTVD  41081  elixpconstg  41235  rabidim2  41249  foelrnf  41327  disjinfi  41334  supminfxr2  41625  sumnnodd  41791  stoweidlem7  42173  stoweidlem14  42180  stoweidlem16  42182  stoweidlem24  42190  stoweidlem31  42197  stoweidlem54  42220  wallispilem3  42233  fourierdlem42  42315  fourierdlem48  42320  fourierdlem51  42323  fourierdlem64  42336  fourierdlem76  42348  fourierdlem79  42351  fourierdlem81  42353  fourierdlem87  42359  etransclem28  42428  etransclem32  42432  sge0fodjrnlem  42579  hoidmvlelem3  42760  pimrecltpos  42868  pimrecltneg  42882  issmflem  42885  smfaddlem1  42920  smfsuplem1  42966  smfsuplem3  42968  smflimsuplem7  42981  smfliminflem  42985  nfunsnafv  43222  faovcl  43280  tz6.12-2-afv2  43317  tz6.12i-afv2  43323  sprel  43493  evendiv2z  43644  oddp1div2z  43645  2dvdseven  43665  2ndvdsodd  43667  perfectALTVlem1  43733  sbgoldbm  43796  clintopcllaw  44016  0ringbas  44040  rnghmmgmhm  44063  uzlidlring  44098  rnghmsubcsetclem1  44144  rngccatidALTV  44158  zrinitorngc  44169  zrtermorngc  44170  rhmsubcsetclem1  44190  funcringcsetcALTV2lem7  44211  ringccatidALTV  44221  funcringcsetclem7ALTV  44234  irinitoringc  44238  zrtermoringc  44239  fldhmsubc  44253  fldhmsubcALTV  44271  ssnn0ssfz  44295  el0ldepsnzr  44420  regt1loggt0  44494  elbigodm  44513  fllogbd  44518  rrx2xpref1o  44603  elsetrecslem  44699
  Copyright terms: Public domain W3C validator