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

Theorem simprbi 479
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 206 . 2 (𝜑 → (𝜓𝜒))
32simprd 478 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  simplbiim  659  xornan  1512  sb1  1940  eumoOLD  2528  reurmo  3191  pssne  3736  pssn2lp  3741  ssnpss  3743  eldifn  3766  elinel2  3833  rabsnt  4298  eldifsni  4353  unimax  4505  ssintub  4527  moop2  4995  pwssun  5049  weso  5134  opelxp2  5185  wfisg  5753  ordwe  5774  funmo  5942  funopg  5960  funun  5970  fununi  6002  funimaexg  6013  fndm  6028  frn  6091  f1ss  6144  f1ssr  6145  f1ssres  6146  forn  6156  f1f1orn  6186  f1orescnv  6190  f1imacnv  6191  funcocnv2  6199  dffv2  6310  exfo  6417  foelrn  6418  isorel  6616  isoini2  6629  f1ofveu  6685  fovcl  6807  f1opw  6931  onminesb  7040  onminsb  7041  tfis  7096  limomss  7112  nnlim  7120  ssnlim  7125  curry1  7314  curry2  7317  f1o2ndf1  7330  fnwelem  7337  ressuppss  7359  mpt2xopn0yelv  7384  wfrlem5  7464  tz7.48lem  7581  dif20el  7630  oeordi  7712  oeeulem  7726  oeeui  7727  nnawordex  7762  swoer  7817  erdisj  7837  eceqoveq  7895  mapsnconst  7945  resixpfo  7988  boxcutc  7993  sdomnen  8026  en0  8060  en1  8064  domunsncan  8101  fodomr  8152  phplem4  8183  php3  8187  unxpdomlem3  8207  fineqvlem  8215  f1opwfi  8311  fsuppcolem  8347  fsuppco  8348  mapfienlem1  8351  mapfienlem2  8352  supub  8406  suplub  8407  ordtypelem2  8465  ordtypelem3  8466  ordtypelem6  8469  ordtypelem7  8470  wemapso2lem  8498  wdom2d  8526  brwdom3  8528  ixpiunwdom  8537  inf3lem2  8564  inf3lem6  8568  oancom  8586  infdifsn  8592  cantnfp1lem3  8615  cantnflem3  8626  cantnflem4  8627  oef1o  8633  cnfcom3  8639  tctr  8654  tz9.12lem3  8690  scottex  8786  cardid2  8817  infxpenlem  8874  acni3  8908  cardaleph  8950  iscard3  8954  dfac5lem4  8987  dfac5lem5  8988  kmlem1  9010  cofsmo  9129  fin4en1  9169  enfin2i  9181  fin23lem28  9200  fin23lem38  9209  isf32lem6  9218  enfin1ai  9244  isfin1-3  9246  hsmexlem2  9287  hsmexlem4  9289  domtriomlem  9302  axdc2lem  9308  axdc3lem2  9311  ac6num  9339  zorn2lem2  9357  brdom3  9388  alephval2  9432  alephreg  9442  pwcfsdom  9443  smobeth  9446  fpwwe2lem6  9495  fpwwe2lem13  9502  canthp1lem2  9513  pwfseqlem3  9520  hargch  9533  winalim2  9556  gchina  9559  inar1  9635  0npi  9742  mulclpi  9753  mulcanpi  9760  nlt1pi  9766  nqereu  9789  prcdnq  9853  prnmax  9855  ltresr2  10000  axrnegex  10021  axpre-sup  10028  eluz2gt1  11798  1nuz2  11802  zsupss  11815  rpgt0  11882  ixxss1  12231  ixxss2  12232  ixxss12  12233  lbioo  12244  ubioo  12245  iccss2  12282  iccssico2  12285  elfzuz3  12377  uzdisj  12451  nn0disj  12494  serge0  12895  expge0  12936  expge1  12937  expaddzlem  12943  hashrabsn1  13201  hashfun  13262  cshinj  13603  relexpuzrel  13836  shftfn  13857  sqrlem6  14032  rlimss  14277  lo1dm  14294  o1dm  14305  rlimrege0  14354  fsumf1o  14498  fsumge0  14571  incexc2  14614  supcvg  14632  fprodf1o  14720  divalglem9  15171  bitsfzolem  15203  bitsinv2  15212  bitsf1ocnv  15213  bitsf1  15215  gcdcllem1  15268  bezout  15307  prmind2  15445  nprm  15448  sqnprm  15461  dvdsprm  15462  isprm5  15466  coprm  15470  phibndlem  15522  dfphi2  15526  phimullem  15531  phisum  15542  pclem  15590  pcpre1  15594  pcidlem  15623  expnprm  15653  prmreclem1  15667  prmreclem2  15668  prmreclem5  15671  1arith  15678  4sqlem18  15713  vdwnnlem3  15748  ramtlecl  15751  rami  15766  0ram  15771  ramub1lem1  15777  prmgaplem5  15806  firest  16140  acsfiel  16362  isacs1i  16365  catlid  16391  catrid  16392  fullfo  16619  fthf1  16624  fthoppc  16630  invfuc  16681  prslem  16978  posi  16997  dlatmjdi  17241  pslem  17253  tsrlin  17266  cnvtsr  17269  tsrdir  17285  mndid  17350  mhmf  17387  mhmlin  17389  mhm0  17390  mrcmndind  17413  grpinvex  17479  grplinv  17515  mulgz  17615  mulgdirlem  17619  mulgdir  17620  mulgass  17626  nsgbi  17672  nmzbi  17681  ghmf  17711  ghmlin  17712  conjnsg  17743  gimf1o  17752  gagrpid  17773  gaf  17774  gaass  17776  psgnunilem5  17960  odid  18003  odf1o2  18034  gexid  18042  sylow1lem4  18062  odcau  18065  pj1id  18158  efgredeu  18211  ablcmn  18245  cmncom  18255  mulgdi  18278  gexexlem  18301  torsubg  18303  cyggenod2  18333  cygctb  18339  ghmcyg  18343  dprdf1o  18477  dprd2dlem1  18486  dprd2da  18487  ablfacrplem  18510  ablfaclem2  18531  ablfac2  18534  crngmgp  18601  rhmmhm  18770  rhmghm  18773  drngunit  18800  drngmgp  18807  drngid  18809  subrgss  18829  subrg1cl  18836  issubdrg  18853  abvge0  18873  srngcnv  18901  lmhmlin  19083  lmimf1o  19111  lvecdrng  19153  lspsolvlem  19190  islbs3  19203  lbsextlem3  19208  2idlcpbl  19282  nzrnz  19308  opprnzr  19313  rrgeq0i  19337  domneq0  19345  domnrrg  19348  drngdomn  19351  fldidom  19353  assalem  19364  mplsubrglem  19487  mplcoe1  19513  mplbas2  19518  opsrtoslem2  19533  mplelsfi  19539  coe1mul2  19687  zringunit  19884  prmirredlem  19889  znidomb  19958  cygzn  19967  psgndiflemB  19994  pjf  20105  frlmsslsp  20183  frlmlbs  20184  f1lindf  20209  pmatcoe1fsupp  20554  toponuni  20767  tpsuni  20788  clsval2  20902  mretopd  20944  neips  20965  neiptoptop  20983  neiptopnei  20984  perflp  21006  perfi  21007  restfpw  21031  cnf  21098  cnpf  21099  cnpimaex  21108  cnima  21117  t0sep  21176  t1ficld  21179  hausnei  21180  pnrmcld  21194  cnrmi  21212  cmpcov  21240  discmp  21249  tgcmp  21252  uncmp  21254  hauscmplem  21257  cmpfi  21259  connclo  21266  1stcclb  21295  2ndcdisj  21307  llyi  21325  nllyi  21326  ptpjpre1  21422  ptpjcn  21462  ptpjopn  21463  ptclsg  21466  dfac14  21469  txdis1cn  21486  pthaus  21489  hauseqlcld  21497  txkgen  21503  xkococn  21511  txconn  21540  hmeocnvcn  21612  fbssfi  21688  filss  21704  ufilss  21756  uffixfr  21774  flimneiss  21817  flimelbas  21819  fclscf  21876  flimfnfcls  21879  alexsublem  21895  alexsubb  21897  alexsubALT  21902  ptcmplem2  21904  ptcmplem3  21905  ptcmplem4  21906  tmdgsum2  21947  ghmcnp  21965  tgpt0  21969  qustgplem  21971  tsmsfbas  21978  tsmslem1  21979  tsmsgsum  21989  tsmssubm  21993  tsmsres  21994  tsmsf1o  21995  tsmsmhm  21996  tsmsadd  21997  tsmsxplem1  22003  tsmsxplem2  22004  tsmsxp  22005  istdrg2  22028  vscacn  22036  tvctdrg  22043  uspreg  22125  ucncn  22136  neipcfilu  22147  cuspcvg  22152  psmetxrge0  22165  isxmet2d  22179  prdsxmetlem  22220  imasdsf1olem  22225  xmstopn  22303  mstopn  22304  stdbdxmet  22367  prdsxmslem2  22381  nrgabv  22512  nmvs  22527  nvclvec  22548  nmoge0  22572  nghmcl  22578  nmoi  22579  nghmghm  22585  nmhmlmhm  22600  nmhmnghm  22601  icccmp  22675  xrge0gsumle  22683  xrge0tsms  22684  metds0  22700  metdstri  22701  metdsre  22703  metdseq0  22704  metdscnlem  22705  metnrmlem1a  22708  icopnfcnv  22788  xrhmeo  22792  pcoval1  22859  cvslvec  22971  cvsunit  22977  cphreccllem  23024  cmetcvg  23129  lmle  23145  cmscmet  23189  cmetcusp1  23195  hlcph  23206  minveclem4  23249  ivthlem3  23268  ovolmge0  23291  ovolicc1  23330  ovolicc2lem3  23333  ovolicc2lem5  23335  mblsplit  23346  dyadmbl  23414  mbfdm  23440  mbfadd  23473  mbfsub  23474  i1ff  23488  i1frn  23489  i1fima2  23491  mbfmul  23538  itg2monolem1  23562  bddmulibl  23650  dvnres  23739  c1liplem1  23804  c1lip2  23806  dvge0  23814  lhop1lem  23821  itgsubstlem  23856  fta1glem1  23970  fta1glem2  23971  fta1b  23974  plyf  23999  plypf1  24013  plyadd  24018  plymul  24019  coeeu  24026  dgrlem  24030  coeid  24039  elqaalem3  24121  aareccl  24126  eff1olem  24339  relogf1o  24358  logdmn0  24431  logcnlem2  24434  logcnlem3  24435  dvloglem  24439  efopnlem1  24447  efopnlem2  24448  logtayl2  24453  cxpcn3lem  24533  cxpcn3  24534  atandmneg  24678  atandmcj  24681  efiatan2  24689  cosatan  24693  cosatanne0  24694  dvatan  24707  areage0  24735  cxp2lim  24748  jensenlem2  24759  jensen  24760  eldmgm  24793  dmgmaddn0  24794  dmlogdmgm  24795  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem5  24804  lgambdd  24808  lgamucov  24809  wilthlem1  24839  wilth  24842  ftalem3  24846  efnnfsumcl  24874  isppw  24885  efchtdvds  24930  sqff1o  24953  fsumdvdsdiaglem  24954  dvdsppwf1o  24957  dvdsflf1o  24958  musum  24962  muinv  24964  dvdsmulf1o  24965  fsumvma2  24984  vmasum  24986  chpval2  24988  chpchtsum  24989  chpub  24990  mersenne  24997  perfect1  24998  bposlem1  25054  lgsfle1  25076  lgsle1  25082  lgsdirprm  25101  lgsne0  25105  lgseisenlem3  25147  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem2  25151  2sqblem  25201  chebbnd1lem1  25203  chebbnd1  25206  chtppilim  25209  chpchtlim  25213  chpo1ub  25214  rplogsumlem2  25219  rpvmasumlem  25221  dchrmusumlema  25227  dchrvmasumlem1  25229  dchrisum0flblem2  25243  dchrisum0lema  25248  dchrisum0lem2a  25251  logsqvma  25276  selberg3lem2  25292  pntrsumo1  25299  pnt2  25347  ostthlem1  25361  ostth3  25372  axtgcgrrflx  25406  axtgcgrid  25407  axtgsegcon  25408  axtg5seg  25409  axtgbtwnid  25410  axtgpasch  25411  axtgcont1  25412  tglng  25486  axcontlem7  25895  axcontlem10  25898  upgrle  26030  umgredg2  26040  lfgredgge2  26064  usgredg2ALT  26130  usgr1vr  26192  usgrexmpledg  26199  upgrres1  26250  fusgrvtxfi  26256  vtxnbuvtx  26339  cusgrcplgr  26372  vdumgr0  26432  vtxdgoddnumeven  26505  trlres  26653  usgr2pth  26716  umgrn1cycl  26755  clwwlknlen  26994  clwlksfclwwlk1hashn  27046  2clwwlk2  27336  ablocom  27530  phpar2  27806  cbncms  27849  hlph  27873  hcaucvg  28171  hlimconvi  28176  shaddcl  28202  shmulcl  28203  chlimi  28219  chcompl  28227  choc1  28314  nmopre  28857  cnopc  28900  lnopl  28901  unop  28902  hmop  28909  cnfnc  28917  lnfnl  28918  nlelshi  29047  cnlnadjlem5  29058  elpjidm  29171  mdslle1i  29304  mdslle2i  29305  atcv0  29329  chpssati  29350  fovcld  29568  aciunf1lem  29590  padct  29625  ssnnssfz  29677  ressprs  29783  oduprs  29784  resspos  29787  resstos  29788  tleile  29789  ogrpinvOLD  29843  ogrpinv0le  29844  ogrpsub  29845  ogrpaddlt  29846  isarchi3  29869  archirng  29870  archirngz  29871  archiabllem1a  29873  archiabllem1b  29874  archiabllem2a  29876  archiabllem2c  29877  archiabllem2b  29878  archiabl  29880  orngsqr  29932  ornglmulle  29933  orngrmulle  29934  ofldtos  29939  ofldlt1  29941  ofldchr  29942  suborng  29943  subofld  29944  isarchiofld  29945  nn0omnd  29969  madjusmdetlem4  30024  qtophaus  30031  crefi  30042  cmpcref  30045  cmppcmp  30053  pcmplfin  30055  tpr2rico  30086  rge0scvg  30123  zrhunitpreima  30150  qqhrhm  30161  esummono  30244  gsumesum  30249  esumrnmpt2  30258  esumpinfval  30263  esumpcvgval  30268  esumpmono  30269  0elsiga  30305  sigaclcu  30308  issgon  30314  inelpisys  30345  ldsysgenld  30351  ldgenpisyslem1  30354  sxuni  30384  isrnmeas  30391  measvuni  30405  measssd  30406  ddemeas  30427  imambfm  30452  elmbfmvol2  30457  dya2icoseg2  30468  omssubaddlem  30489  omssubadd  30490  carsgsigalem  30505  pmeasmono  30514  sibfinima  30529  oddpwdc  30544  oddpwdcv  30545  eulerpartlemf  30560  eulerpartlemt  30561  eulerpartlemr  30564  eulerpartlemgvv  30566  eulerpartlemgs2  30570  fiblem  30588  probtot  30602  ballotlem4  30688  ballotlem5  30689  ballotlemfrc  30716  ballotlemirc  30721  ballotth  30727  hgt750lemb  30862  bnj642  30944  bnj643  30945  bnj645  30946  bnj707  30951  bnj1379  31027  bnj1538  31051  bnj110  31054  bnj93  31059  bnj906  31126  bnj1006  31155  bnj1110  31176  bnj1121  31179  bnj1204  31206  bnj1321  31221  bnj1364  31222  bnj1398  31228  bnj1450  31244  bnj1312  31252  bnj1501  31261  bnj1523  31265  subfacp1lem3  31290  subfacp1lem5  31292  pconncn  31332  connpconn  31343  cvmcov  31371  cvmliftlem1  31393  cvmliftlem10  31402  cvmlift2lem11  31421  cvmlift2lem12  31422  msubff1  31579  mvhf1  31582  mthmpps  31605  mclspps  31607  fundmpss  31790  tfisg  31840  frpoinsg  31866  frinsg  31870  frrlem5  31909  sltval2  31934  txpss3v  32110  pprodss4v  32116  fnetg  32465  neibastop1  32479  filnetlem3  32500  onint1  32573  bj-elid2  33216  icorempt2  33329  wl-nfeqfb  33453  phpreu  33523  fin2solem  33525  fin2so  33526  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  matunitlindf  33537  ptrest  33538  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  poimirlem31  33570  mblfinlem2  33577  dvtan  33590  itg2gt0cn  33595  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  cover2  33638  indexa  33658  istotbnd3  33700  sstotbnd2  33703  sstotbnd  33704  totbndss  33706  equivtotbnd  33707  isbnd3  33713  totbndbnd  33718  equivbnd  33719  prdsbnd  33722  prdstotbnd  33723  heibor  33750  zrdivrng  33882  crngocom  33930  isfld2  33934  dmncrng  33985  xrnss3v  34274  prter2  34485  toycom  34578  lsateln0  34600  lpssat  34618  lssat  34621  oposlem  34787  olop  34819  omllaw  34848  cvlexch1  34933  dihpN  36942  mapdordlem2  37243  nacsfg  37585  nacsfix  37592  mzpindd  37626  diophrw  37639  diophrex  37656  rexzrexnn0  37685  pell1234qrdich  37742  rmspecsqrtnqOLD  37788  rmspecnonsq  37789  rmspecfund  37791  rmspecpos  37798  monotoddzzfi  37824  ltrmxnn0  37833  rmxnn  37835  jm2.23  37880  jm3.1lem2  37902  dnnumch3  37934  lnmlssfg  37967  lnmlmic  37975  lnrlnm  38000  lnr2i  38003  lpirlnr  38004  hbtlem6  38016  hbt  38017  mnccoe  38025  cntzsdrg  38089  idomrootle  38090  proot1mul  38094  proot1hash  38095  deg1mhm  38102  ntrneifv2  38695  radcnvrat  38830  binomcxplemdvbinom  38869  binomcxplemcvg  38870  binomcxplemnotnn0  38872  ordelordALT  39064  2uasbanh  39094  ordelordALTVD  39417  elixpconstg  39580  rabidim2  39598  foelrnf  39687  disjinfi  39694  supminfxr2  40012  sumnnodd  40180  stoweidlem7  40542  stoweidlem14  40549  stoweidlem16  40551  stoweidlem24  40559  stoweidlem31  40566  stoweidlem54  40589  wallispilem3  40602  fourierdlem42  40684  fourierdlem48  40689  fourierdlem51  40692  fourierdlem64  40705  fourierdlem76  40717  fourierdlem79  40720  fourierdlem81  40722  fourierdlem87  40728  etransclem28  40797  etransclem32  40801  sge0fodjrnlem  40951  hoidmvlelem3  41132  preimagelt  41233  preimalegt  41234  pimrecltpos  41240  pimrecltneg  41254  issmflem  41257  smfaddlem1  41292  smfsuplem1  41338  smfsuplem3  41340  smflimsuplem7  41353  smfliminflem  41357  nfunsnafv  41543  faovcl  41601  evendiv2z  41870  oddp1div2z  41871  2dvdseven  41891  2ndvdsodd  41892  perfectALTVlem1  41955  sbgoldbm  41997  sprel  42059  clintopcllaw  42172  0ringbas  42196  rnghmmgmhm  42219  uzlidlring  42254  rnghmsubcsetclem1  42300  rngccatidALTV  42314  zrinitorngc  42325  zrtermorngc  42326  rhmsubcsetclem1  42346  funcringcsetcALTV2lem7  42367  ringccatidALTV  42377  funcringcsetclem7ALTV  42390  irinitoringc  42394  zrtermoringc  42395  fldhmsubc  42409  fldhmsubcALTV  42427  ssnn0ssfz  42452  el0ldepsnzr  42581  regt1loggt0  42655  elbigodm  42674  fllogbd  42679  elsetrecslem  42770
  Copyright terms: Public domain W3C validator