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

Theorem simprbi 483
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 482 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  661  xornan  1617  sb1  2045  eumoOLD  2633  reurmo  3296  pssne  3841  pssn2lp  3846  ssnpss  3848  eldifn  3872  elinel2  3939  rabsnt  4406  eldifsni  4462  unimax  4621  ssintub  4643  moop2  5110  pwssun  5166  weso  5253  opelxp2  5304  wfisg  5872  ordwe  5893  funmo  6061  funopg  6079  funun  6089  fununi  6121  funimaexg  6132  fndm  6147  frn  6210  f1ss  6263  f1ssr  6264  f1ssres  6265  forn  6275  f1f1orn  6305  f1orescnv  6309  f1imacnv  6310  funcocnv2  6318  dffv2  6429  exfo  6536  foelrn  6537  isorel  6735  isoini2  6748  f1ofveu  6804  fovcl  6926  f1opw  7050  onminesb  7159  onminsb  7160  tfis  7215  limomss  7231  nnlim  7239  ssnlim  7244  curry1  7433  curry2  7436  f1o2ndf1  7449  fnwelem  7456  ressuppss  7478  mpt2xopn0yelv  7504  wfrlem5  7584  tz7.48lem  7701  dif20el  7750  oeordi  7832  oeeulem  7846  oeeui  7847  nnawordex  7882  swoer  7937  erdisj  7957  eceqoveq  8015  mapsnconst  8065  resixpfo  8108  boxcutc  8113  sdomnen  8146  en0  8180  en1  8184  domunsncan  8221  fodomr  8272  phplem4  8303  php3  8307  unxpdomlem3  8327  fineqvlem  8335  f1opwfi  8431  fsuppcolem  8467  fsuppco  8468  mapfienlem1  8471  mapfienlem2  8472  supub  8526  suplub  8527  ordtypelem2  8585  ordtypelem3  8586  ordtypelem6  8589  ordtypelem7  8590  wemapso2lem  8618  wdom2d  8646  brwdom3  8648  ixpiunwdom  8657  inf3lem2  8695  inf3lem6  8699  oancom  8717  infdifsn  8723  cantnfp1lem3  8746  cantnflem3  8757  cantnflem4  8758  oef1o  8764  cnfcom3  8770  tctr  8785  tz9.12lem3  8821  scottex  8917  cardid2  8965  infxpenlem  9022  acni3  9056  cardaleph  9098  iscard3  9102  dfac5lem4  9135  dfac5lem5  9136  kmlem1  9160  cofsmo  9279  fin4en1  9319  enfin2i  9331  fin23lem28  9350  fin23lem38  9359  isf32lem6  9368  enfin1ai  9394  isfin1-3  9396  hsmexlem2  9437  hsmexlem4  9439  domtriomlem  9452  axdc2lem  9458  axdc3lem2  9461  ac6num  9489  zorn2lem2  9507  brdom3  9538  alephval2  9582  alephreg  9592  pwcfsdom  9593  smobeth  9596  fpwwe2lem6  9645  fpwwe2lem13  9652  canthp1lem2  9663  pwfseqlem3  9670  hargch  9683  winalim2  9706  gchina  9709  inar1  9785  0npi  9892  mulclpi  9903  mulcanpi  9910  nlt1pi  9916  nqereu  9939  prcdnq  10003  prnmax  10005  ltresr2  10150  axrnegex  10171  axpre-sup  10178  eluz2gt1  11949  1nuz2  11953  zsupss  11966  rpgt0  12033  ixxss1  12382  ixxss2  12383  ixxss12  12384  lbioo  12395  ubioo  12396  iccss2  12433  iccssico2  12436  elfzuz3  12528  uzdisj  12602  nn0disj  12645  serge0  13045  expge0  13086  expge1  13087  expaddzlem  13093  hashrabsn1  13351  hashfun  13412  cshinj  13753  relexpuzrel  13987  shftfn  14008  sqrlem6  14183  rlimss  14428  lo1dm  14445  o1dm  14456  rlimrege0  14505  fsumf1o  14649  fsumge0  14722  incexc2  14765  supcvg  14783  fprodf1o  14871  divalglem9  15322  bitsfzolem  15354  bitsinv2  15363  bitsf1ocnv  15364  bitsf1  15366  gcdcllem1  15419  bezout  15458  prmind2  15596  nprm  15599  sqnprm  15612  dvdsprm  15613  isprm5  15617  coprm  15621  phibndlem  15673  dfphi2  15677  phimullem  15682  phisum  15693  pclem  15741  pcpre1  15745  pcidlem  15774  expnprm  15804  prmreclem1  15818  prmreclem2  15819  prmreclem5  15822  1arith  15829  4sqlem18  15864  vdwnnlem3  15899  ramtlecl  15902  rami  15917  0ram  15922  ramub1lem1  15928  prmgaplem5  15957  firest  16291  acsfiel  16512  isacs1i  16515  catlid  16541  catrid  16542  fullfo  16769  fthf1  16774  fthoppc  16780  invfuc  16831  prslem  17128  posi  17147  dlatmjdi  17391  pslem  17403  tsrlin  17416  cnvtsr  17419  tsrdir  17435  mndid  17500  mhmf  17537  mhmlin  17539  mhm0  17540  mrcmndind  17563  grpinvex  17629  grplinv  17665  mulgz  17765  mulgdirlem  17769  mulgdir  17770  mulgass  17776  nsgbi  17822  nmzbi  17831  ghmf  17861  ghmlin  17862  conjnsg  17893  gimf1o  17902  gagrpid  17923  gaf  17924  gaass  17926  psgnunilem5  18110  odid  18153  odf1o2  18184  gexid  18192  sylow1lem4  18212  odcau  18215  pj1id  18308  efgredeu  18361  ablcmn  18395  cmncom  18405  mulgdi  18428  gexexlem  18451  torsubg  18453  cyggenod2  18483  cygctb  18489  ghmcyg  18493  dprdf1o  18627  dprd2dlem1  18636  dprd2da  18637  ablfacrplem  18660  ablfaclem2  18681  ablfac2  18684  crngmgp  18751  rhmmhm  18920  rhmghm  18923  drngunit  18950  drngmgp  18957  drngid  18959  subrgss  18979  subrg1cl  18986  issubdrg  19003  abvge0  19023  srngcnv  19051  lmhmlin  19233  lmimf1o  19261  lvecdrng  19303  lspsolvlem  19340  islbs3  19353  lbsextlem3  19358  2idlcpbl  19432  nzrnz  19458  opprnzr  19463  rrgeq0i  19487  domneq0  19495  domnrrg  19498  drngdomn  19501  fldidom  19503  assalem  19514  mplsubrglem  19637  mplcoe1  19663  mplbas2  19668  opsrtoslem2  19683  mplelsfi  19689  coe1mul2  19837  zringunit  20034  prmirredlem  20039  znidomb  20108  cygzn  20117  psgndiflemB  20144  pjf  20255  frlmsslsp  20333  frlmlbs  20334  f1lindf  20359  pmatcoe1fsupp  20704  toponuni  20917  tpsuni  20938  clsval2  21052  mretopd  21094  neips  21115  neiptoptop  21133  neiptopnei  21134  perflp  21156  perfi  21157  restfpw  21181  cnf  21248  cnpf  21249  cnpimaex  21258  cnima  21267  t0sep  21326  t1ficld  21329  hausnei  21330  pnrmcld  21344  cnrmi  21362  cmpcov  21390  discmp  21399  tgcmp  21402  uncmp  21404  hauscmplem  21407  cmpfi  21409  connclo  21416  1stcclb  21445  2ndcdisj  21457  llyi  21475  nllyi  21476  ptpjpre1  21572  ptpjcn  21612  ptpjopn  21613  ptclsg  21616  dfac14  21619  txdis1cn  21636  pthaus  21639  hauseqlcld  21647  txkgen  21653  xkococn  21661  txconn  21690  hmeocnvcn  21762  fbssfi  21838  filss  21854  ufilss  21906  uffixfr  21924  flimneiss  21967  flimelbas  21969  fclscf  22026  flimfnfcls  22029  alexsublem  22045  alexsubb  22047  alexsubALT  22052  ptcmplem2  22054  ptcmplem3  22055  ptcmplem4  22056  tmdgsum2  22097  ghmcnp  22115  tgpt0  22119  qustgplem  22121  tsmsfbas  22128  tsmslem1  22129  tsmsgsum  22139  tsmssubm  22143  tsmsres  22144  tsmsf1o  22145  tsmsmhm  22146  tsmsadd  22147  tsmsxplem1  22153  tsmsxplem2  22154  tsmsxp  22155  istdrg2  22178  vscacn  22186  tvctdrg  22193  uspreg  22275  ucncn  22286  neipcfilu  22297  cuspcvg  22302  psmetxrge0  22315  isxmet2d  22329  prdsxmetlem  22370  imasdsf1olem  22375  xmstopn  22453  mstopn  22454  stdbdxmet  22517  prdsxmslem2  22531  nrgabv  22662  nmvs  22677  nvclvec  22698  nmoge0  22722  nghmcl  22728  nmoi  22729  nghmghm  22735  nmhmlmhm  22750  nmhmnghm  22751  icccmp  22825  xrge0gsumle  22833  xrge0tsms  22834  metds0  22850  metdstri  22851  metdsre  22853  metdseq0  22854  metdscnlem  22855  metnrmlem1a  22858  icopnfcnv  22938  xrhmeo  22942  pcoval1  23009  cvslvec  23121  cvsunit  23127  cphreccllem  23174  cmetcvg  23279  lmle  23295  cmscmet  23339  cmetcusp1  23345  hlcph  23356  minveclem4  23399  ivthlem3  23418  ovolmge0  23441  ovolicc1  23480  ovolicc2lem3  23483  ovolicc2lem5  23485  mblsplit  23496  dyadmbl  23564  mbfdm  23590  mbfadd  23623  mbfsub  23624  i1ff  23638  i1frn  23639  i1fima2  23641  mbfmul  23688  itg2monolem1  23712  bddmulibl  23800  dvnres  23889  c1liplem1  23954  c1lip2  23956  dvge0  23964  lhop1lem  23971  itgsubstlem  24006  fta1glem1  24120  fta1glem2  24121  fta1b  24124  plyf  24149  plypf1  24163  plyadd  24168  plymul  24169  coeeu  24176  dgrlem  24180  coeid  24189  elqaalem3  24271  aareccl  24276  eff1olem  24489  relogf1o  24508  logdmn0  24581  logcnlem2  24584  logcnlem3  24585  dvloglem  24589  efopnlem1  24597  efopnlem2  24598  logtayl2  24603  cxpcn3lem  24683  cxpcn3  24684  atandmneg  24828  atandmcj  24831  efiatan2  24839  cosatan  24843  cosatanne0  24844  dvatan  24857  areage0  24885  cxp2lim  24898  jensenlem2  24909  jensen  24910  eldmgm  24943  dmgmaddn0  24944  dmlogdmgm  24945  lgamgulmlem2  24951  lgamgulmlem3  24952  lgamgulmlem5  24954  lgambdd  24958  lgamucov  24959  wilthlem1  24989  wilth  24992  ftalem3  24996  efnnfsumcl  25024  isppw  25035  efchtdvds  25080  sqff1o  25103  fsumdvdsdiaglem  25104  dvdsppwf1o  25107  dvdsflf1o  25108  musum  25112  muinv  25114  dvdsmulf1o  25115  fsumvma2  25134  vmasum  25136  chpval2  25138  chpchtsum  25139  chpub  25140  mersenne  25147  perfect1  25148  bposlem1  25204  lgsfle1  25226  lgsle1  25232  lgsdirprm  25251  lgsne0  25255  lgseisenlem3  25297  lgseisenlem4  25298  lgsquadlem1  25300  lgsquadlem2  25301  2sqblem  25351  chebbnd1lem1  25353  chebbnd1  25356  chtppilim  25359  chpchtlim  25363  chpo1ub  25364  rplogsumlem2  25369  rpvmasumlem  25371  dchrmusumlema  25377  dchrvmasumlem1  25379  dchrisum0flblem2  25393  dchrisum0lema  25398  dchrisum0lem2a  25401  logsqvma  25426  selberg3lem2  25442  pntrsumo1  25449  pnt2  25497  ostthlem1  25511  ostth3  25522  axtgcgrrflx  25556  axtgcgrid  25557  axtgsegcon  25558  axtg5seg  25559  axtgbtwnid  25560  axtgpasch  25561  axtgcont1  25562  tglng  25636  axcontlem7  26045  axcontlem10  26048  upgrle  26180  umgredg2  26190  lfgredgge2  26214  usgredg2ALT  26280  usgr1vr  26342  usgrexmpledg  26349  upgrres1  26400  fusgrvtxfi  26406  vtxnbuvtx  26489  cusgrcplgr  26522  vdumgr0  26582  vtxdgoddnumeven  26655  trlres  26803  usgr2pth  26866  umgrn1cycl  26906  clwwlknlen  27156  clwlksfclwwlk1hashnOLD  27209  clwwnonrepclwwnon  27498  2clwwlk2  27501  ablocom  27707  phpar2  27983  cbncms  28026  hlph  28050  hcaucvg  28348  hlimconvi  28353  shaddcl  28379  shmulcl  28380  chlimi  28396  chcompl  28404  choc1  28491  nmopre  29034  cnopc  29077  lnopl  29078  unop  29079  hmop  29086  cnfnc  29094  lnfnl  29095  nlelshi  29224  cnlnadjlem5  29235  elpjidm  29348  mdslle1i  29481  mdslle2i  29482  atcv0  29506  chpssati  29527  fovcld  29745  aciunf1lem  29767  padct  29802  ssnnssfz  29854  ressprs  29960  oduprs  29961  resspos  29964  resstos  29965  tleile  29966  ogrpinvOLD  30020  ogrpinv0le  30021  ogrpsub  30022  ogrpaddlt  30023  isarchi3  30046  archirng  30047  archirngz  30048  archiabllem1a  30050  archiabllem1b  30051  archiabllem2a  30053  archiabllem2c  30054  archiabllem2b  30055  archiabl  30057  orngsqr  30109  ornglmulle  30110  orngrmulle  30111  ofldtos  30116  ofldlt1  30118  ofldchr  30119  suborng  30120  subofld  30121  isarchiofld  30122  nn0omnd  30146  madjusmdetlem4  30201  qtophaus  30208  crefi  30219  cmpcref  30222  cmppcmp  30230  pcmplfin  30232  tpr2rico  30263  rge0scvg  30300  zrhunitpreima  30327  qqhrhm  30338  esummono  30421  gsumesum  30426  esumrnmpt2  30435  esumpinfval  30440  esumpcvgval  30445  esumpmono  30446  0elsiga  30482  sigaclcu  30485  issgon  30491  inelpisys  30522  ldsysgenld  30528  ldgenpisyslem1  30531  sxuni  30561  isrnmeas  30568  measvuni  30582  measssd  30583  ddemeas  30604  imambfm  30629  elmbfmvol2  30634  dya2icoseg2  30645  omssubaddlem  30666  omssubadd  30667  carsgsigalem  30682  pmeasmono  30691  sibfinima  30706  oddpwdc  30721  oddpwdcv  30722  eulerpartlemf  30737  eulerpartlemt  30738  eulerpartlemr  30741  eulerpartlemgvv  30743  eulerpartlemgs2  30747  fiblem  30765  probtot  30779  ballotlem4  30865  ballotlem5  30866  ballotlemfrc  30893  ballotlemirc  30898  ballotth  30904  hgt750lemb  31039  bnj642  31121  bnj643  31122  bnj645  31123  bnj707  31128  bnj1379  31204  bnj1538  31228  bnj110  31231  bnj93  31236  bnj906  31303  bnj1006  31332  bnj1110  31353  bnj1121  31356  bnj1204  31383  bnj1321  31398  bnj1364  31399  bnj1398  31405  bnj1450  31421  bnj1312  31429  bnj1501  31438  bnj1523  31442  subfacp1lem3  31467  subfacp1lem5  31469  pconncn  31509  connpconn  31520  cvmcov  31548  cvmliftlem1  31570  cvmliftlem10  31579  cvmlift2lem11  31598  cvmlift2lem12  31599  msubff1  31756  mvhf1  31759  mthmpps  31782  mclspps  31784  fundmpss  31967  tfisg  32017  frpoinsg  32043  frinsg  32047  frrlem5  32086  sltval2  32111  txpss3v  32287  pprodss4v  32293  fnetg  32642  neibastop1  32656  filnetlem3  32677  onint1  32750  bj-elid2  33393  icorempt2  33506  wl-nfeqfb  33632  phpreu  33702  fin2solem  33704  fin2so  33705  lindsenlbs  33713  matunitlindflem1  33714  matunitlindflem2  33715  matunitlindf  33716  ptrest  33717  poimirlem1  33719  poimirlem2  33720  poimirlem3  33721  poimirlem4  33722  poimirlem5  33723  poimirlem6  33724  poimirlem7  33725  poimirlem8  33726  poimirlem9  33727  poimirlem10  33728  poimirlem11  33729  poimirlem12  33730  poimirlem13  33731  poimirlem14  33732  poimirlem15  33733  poimirlem16  33734  poimirlem17  33735  poimirlem18  33736  poimirlem19  33737  poimirlem20  33738  poimirlem21  33739  poimirlem22  33740  poimirlem23  33741  poimirlem24  33742  poimirlem26  33744  poimirlem27  33745  poimirlem29  33747  poimirlem31  33749  mblfinlem2  33756  dvtan  33769  itg2gt0cn  33774  ftc1anclem7  33800  ftc1anclem8  33801  ftc1anc  33802  cover2  33817  indexa  33837  istotbnd3  33879  sstotbnd2  33882  sstotbnd  33883  totbndss  33885  equivtotbnd  33886  isbnd3  33892  totbndbnd  33897  equivbnd  33898  prdsbnd  33901  prdstotbnd  33902  heibor  33929  zrdivrng  34061  crngocom  34109  isfld2  34113  dmncrng  34164  xrnss3v  34453  prter2  34666  toycom  34759  lsateln0  34781  lpssat  34799  lssat  34802  oposlem  34968  olop  35000  omllaw  35029  cvlexch1  35114  dihpN  37123  mapdordlem2  37424  nacsfg  37766  nacsfix  37773  mzpindd  37807  diophrw  37820  diophrex  37837  rexzrexnn0  37866  pell1234qrdich  37923  rmspecsqrtnqOLD  37969  rmspecnonsq  37970  rmspecfund  37972  rmspecpos  37979  monotoddzzfi  38005  ltrmxnn0  38014  rmxnn  38016  jm2.23  38061  jm3.1lem2  38083  dnnumch3  38115  lnmlssfg  38148  lnmlmic  38156  lnrlnm  38181  lnr2i  38184  lpirlnr  38185  hbtlem6  38197  hbt  38198  mnccoe  38206  cntzsdrg  38270  idomrootle  38271  proot1mul  38275  proot1hash  38276  deg1mhm  38283  ntrneifv2  38876  radcnvrat  39011  binomcxplemdvbinom  39050  binomcxplemcvg  39051  binomcxplemnotnn0  39053  ordelordALT  39245  2uasbanh  39275  ordelordALTVD  39598  elixpconstg  39761  rabidim2  39779  foelrnf  39868  disjinfi  39875  supminfxr2  40193  sumnnodd  40361  stoweidlem7  40723  stoweidlem14  40730  stoweidlem16  40732  stoweidlem24  40740  stoweidlem31  40747  stoweidlem54  40770  wallispilem3  40783  fourierdlem42  40865  fourierdlem48  40870  fourierdlem51  40873  fourierdlem64  40886  fourierdlem76  40898  fourierdlem79  40901  fourierdlem81  40903  fourierdlem87  40909  etransclem28  40978  etransclem32  40982  sge0fodjrnlem  41132  hoidmvlelem3  41313  preimagelt  41414  preimalegt  41415  pimrecltpos  41421  pimrecltneg  41435  issmflem  41438  smfaddlem1  41473  smfsuplem1  41519  smfsuplem3  41521  smflimsuplem7  41534  smfliminflem  41538  nfunsnafv  41724  faovcl  41782  evendiv2z  42051  oddp1div2z  42052  2dvdseven  42072  2ndvdsodd  42073  perfectALTVlem1  42136  sbgoldbm  42178  sprel  42240  clintopcllaw  42353  0ringbas  42377  rnghmmgmhm  42400  uzlidlring  42435  rnghmsubcsetclem1  42481  rngccatidALTV  42495  zrinitorngc  42506  zrtermorngc  42507  rhmsubcsetclem1  42527  funcringcsetcALTV2lem7  42548  ringccatidALTV  42558  funcringcsetclem7ALTV  42571  irinitoringc  42575  zrtermoringc  42576  fldhmsubc  42590  fldhmsubcALTV  42608  ssnn0ssfz  42633  el0ldepsnzr  42762  regt1loggt0  42836  elbigodm  42855  fllogbd  42860  elsetrecslem  42951
  Copyright terms: Public domain W3C validator