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

Theorem simprbi 478
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 204 . 2 (𝜑 → (𝜓𝜒))
32simprd 477 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  xornan  1463  sb1  1869  eumo  2486  reurmo  3137  pssne  3664  pssn2lp  3669  ssnpss  3671  eldifn  3694  elinel2  3761  rabsnt  4209  eldifsni  4260  unimax  4403  ssintub  4424  moop2  4885  pwssun  4934  weso  5019  opelxp2  5065  wfisg  5618  ordwe  5639  funmo  5806  funopg  5822  funun  5832  fununi  5864  funimaexg  5875  fndm  5890  frn  5952  f1ss  6004  f1ssr  6005  f1ssres  6006  forn  6016  f1f1orn  6046  f1orescnv  6050  f1imacnv  6051  funcocnv2  6059  dffv2  6166  exfo  6270  foelrn  6271  isorel  6454  isoini2  6467  f1ofveu  6522  fovcl  6641  f1opw  6764  onminesb  6867  onminsb  6868  tfis  6923  limomss  6939  nnlim  6947  ssnlim  6952  curry1  7133  curry2  7136  f1o2ndf1  7149  fnwelem  7156  ressuppss  7178  mpt2xopn0yelv  7203  wfrlem5  7283  tz7.48lem  7400  dif20el  7449  oeordi  7531  oeeulem  7545  oeeui  7546  nnawordex  7581  swoer  7636  erdisj  7658  eceqoveq  7717  mapsnconst  7766  ixpn0  7803  resixpfo  7809  boxcutc  7814  sdomnen  7847  en0  7882  en1  7886  domunsncan  7922  fodomr  7973  phplem4  8004  php3  8008  unxpdomlem3  8028  fineqvlem  8036  f1opwfi  8130  fsuppcolem  8166  fsuppco  8167  mapfienlem1  8170  mapfienlem2  8171  supub  8225  suplub  8226  ordtypelem2  8284  ordtypelem3  8285  ordtypelem6  8288  ordtypelem7  8289  wemapso2lem  8317  wdom2d  8345  brwdom3  8347  ixpiunwdom  8356  inf3lem2  8386  inf3lem6  8390  oancom  8408  infdifsn  8414  cantnfp1lem3  8437  cantnflem3  8448  cantnflem4  8449  oef1o  8455  cnfcom3  8461  tctr  8476  tz9.12lem3  8512  scottex  8608  cardid2  8639  infxpenlem  8696  acni3  8730  cardaleph  8772  iscard3  8776  dfac5lem4  8809  dfac5lem5  8810  kmlem1  8832  cofsmo  8951  fin4en1  8991  enfin2i  9003  fin23lem28  9022  fin23lem38  9031  isf32lem6  9040  enfin1ai  9066  isfin1-3  9068  hsmexlem2  9109  hsmexlem4  9111  domtriomlem  9124  axdc2lem  9130  axdc3lem2  9133  ac6num  9161  zorn2lem2  9179  brdom3  9208  alephval2  9250  alephreg  9260  pwcfsdom  9261  smobeth  9264  fpwwe2lem6  9313  fpwwe2lem13  9320  canthp1lem2  9331  pwfseqlem3  9338  hargch  9351  winalim2  9374  gchina  9377  inar1  9453  0npi  9560  mulclpi  9571  mulcanpi  9578  nlt1pi  9584  nqereu  9607  prcdnq  9671  prnmax  9673  ltresr2  9818  axrnegex  9839  axpre-sup  9846  eluz2gt1  11592  1nuz2  11596  zsupss  11609  rpgt0  11676  ixxss1  12020  ixxss2  12021  ixxss12  12022  lbioo  12033  ubioo  12034  iccss2  12071  iccssico2  12074  elfzuz3  12165  uzdisj  12237  nn0disj  12279  serge0  12672  expge0  12713  expge1  12714  expaddzlem  12720  hashrabsn1  12976  hashfun  13036  cshinj  13354  relexpuzrel  13586  shftfn  13607  sqrlem6  13782  rlimss  14027  lo1dm  14044  o1dm  14055  rlimrege0  14104  fsumf1o  14247  fsumge0  14314  incexc2  14355  supcvg  14373  fprodf1o  14461  divalglem9  14908  bitsfzolem  14940  bitsinv2  14949  bitsf1ocnv  14950  bitsf1  14952  gcdcllem1  15005  bezout  15044  prmind2  15182  nprm  15185  sqnprm  15198  dvdsprm  15199  isprm5  15203  coprm  15207  phibndlem  15259  dfphi2  15263  phimullem  15268  phisum  15279  pclem  15327  pcpre1  15331  pcidlem  15360  expnprm  15390  prmreclem1  15404  prmreclem2  15405  prmreclem5  15408  1arith  15415  4sqlem18  15450  vdwnnlem3  15485  ramtlecl  15488  rami  15503  0ram  15508  ramub1lem1  15514  prmgaplem5  15543  firest  15862  acsfiel  16084  isacs1i  16087  catlid  16113  catrid  16114  fullfo  16341  fthf1  16346  fthoppc  16352  invfuc  16403  prslem  16700  posi  16719  dlatmjdi  16963  pslem  16975  tsrlin  16988  cnvtsr  16991  tsrdir  17007  mndid  17072  mhmf  17109  mhmlin  17111  mhm0  17112  mrcmndind  17135  grpinvex  17201  grplinv  17237  mulgz  17337  mulgdirlem  17341  mulgdir  17342  mulgass  17348  nsgbi  17394  nmzbi  17403  ghmf  17433  ghmlin  17434  conjnsg  17465  gimf1o  17474  gagrpid  17496  gaf  17497  gaass  17499  psgnunilem5  17683  odid  17726  odf1o2  17757  gexid  17765  sylow1lem4  17785  odcau  17788  pj1id  17881  efgredeu  17934  ablcmn  17968  cmncom  17978  mulgdi  18001  gexexlem  18024  torsubg  18026  cyggenod2  18056  cygctb  18062  ghmcyg  18066  dprdf1o  18200  dprd2dlem1  18209  dprd2da  18210  ablfacrplem  18233  ablfaclem2  18254  ablfac2  18257  crngmgp  18324  rhmmhm  18491  rhmghm  18494  drngunit  18521  drngmgp  18528  drngid  18530  subrgss  18550  subrg1cl  18557  issubdrg  18574  abvge0  18594  srngcnv  18622  lmhmlin  18802  lmimf1o  18830  lvecdrng  18872  lspsolvlem  18909  islbs3  18922  lbsextlem3  18927  2idlcpbl  19001  nzrnz  19027  opprnzr  19032  rrgeq0i  19056  domneq0  19064  domnrrg  19067  drngdomn  19070  fldidom  19072  assalem  19083  mplsubrglem  19206  mplcoe1  19232  mplbas2  19237  opsrtoslem2  19252  mplelsfi  19258  coe1mul2  19406  zringunit  19603  prmirredlem  19605  znidomb  19674  cygzn  19683  psgndiflemB  19710  pjf  19818  frlmsslsp  19896  frlmlbs  19897  f1lindf  19922  pmatcoe1fsupp  20267  toponuni  20484  tpsuni  20495  clsval2  20606  mretopd  20648  neips  20669  neiptoptop  20687  neiptopnei  20688  perflp  20710  perfi  20711  restfpw  20735  cnf  20802  cnpf  20803  cnpimaex  20812  cnima  20821  t0sep  20880  t1sncld  20882  t1ficld  20883  hausnei  20884  regsep  20890  pnrmcld  20898  nrmsep3  20911  cnrmi  20916  cmpcov  20944  discmp  20953  tgcmp  20956  uncmp  20958  hauscmplem  20961  cmpfi  20963  conclo  20970  1stcclb  20999  2ndcdisj  21011  llyi  21029  nllyi  21030  ptpjpre1  21126  ptpjcn  21166  ptpjopn  21167  ptclsg  21170  dfac14  21173  txdis1cn  21190  pthaus  21193  hauseqlcld  21201  txkgen  21207  xkococn  21215  txcon  21244  hmeocnvcn  21316  fbssfi  21393  filss  21409  ufilss  21461  uffixfr  21479  flimneiss  21522  flimelbas  21524  fclscf  21581  flimfnfcls  21584  alexsublem  21600  alexsubb  21602  alexsubALT  21607  ptcmplem2  21609  ptcmplem3  21610  ptcmplem4  21611  tmdgsum2  21652  ghmcnp  21670  tgpt0  21674  qustgplem  21676  tsmsfbas  21683  tsmslem1  21684  tsmsgsum  21694  tsmssubm  21698  tsmsres  21699  tsmsf1o  21700  tsmsmhm  21701  tsmsadd  21702  tsmsxplem1  21708  tsmsxplem2  21709  tsmsxp  21710  istdrg2  21733  vscacn  21741  tvctdrg  21748  uspreg  21830  ucncn  21841  neipcfilu  21852  cuspcvg  21857  psmetxrge0  21870  isxmet2d  21883  prdsxmetlem  21924  imasdsf1olem  21929  xmstopn  22007  mstopn  22008  stdbdxmet  22071  prdsxmslem2  22085  nrgabv  22208  nmvs  22223  nvclvec  22244  nmoge0  22267  nghmcl  22273  nmoi  22274  nghmghm  22280  nmhmlmhm  22295  nmhmnghm  22296  icccmp  22368  xrge0gsumle  22376  xrge0tsms  22377  metds0  22392  metdstri  22393  metdsre  22395  metdseq0  22396  metdscnlem  22397  metnrmlem1a  22400  icopnfcnv  22480  xrhmeo  22484  pcoval1  22552  cvslvec  22662  cvsunit  22668  cphreccllem  22710  cmetcvg  22809  lmle  22825  cmscmet  22868  cmetcusp1  22874  hlcph  22885  minveclem4  22928  ivthlem3  22946  ovolmge0  22969  ovolicc1  23008  ovolicc2lem3  23011  ovolicc2lem5  23013  mblsplit  23024  dyadmbl  23091  mbfdm  23118  mbfadd  23151  mbfsub  23152  i1ff  23166  i1frn  23167  i1fima2  23169  mbfmul  23216  itg2monolem1  23240  bddmulibl  23328  dvnres  23417  c1liplem1  23480  c1lip2  23482  dvge0  23490  lhop1lem  23497  itgsubstlem  23532  fta1glem1  23646  fta1glem2  23647  fta1b  23650  plyf  23675  plypf1  23689  plyadd  23694  plymul  23695  coeeu  23702  dgrlem  23706  coeid  23715  elqaalem3  23797  aareccl  23802  eff1olem  24015  relogf1o  24034  logdmn0  24103  logcnlem2  24106  logcnlem3  24107  dvloglem  24111  efopnlem1  24119  efopnlem2  24120  logtayl2  24125  cxpcn3lem  24205  cxpcn3  24206  atandmneg  24350  atandmcj  24353  efiatan2  24361  cosatan  24365  cosatanne0  24366  dvatan  24379  areage0  24407  cxp2lim  24420  jensenlem2  24431  jensen  24432  eldmgm  24465  dmgmaddn0  24466  dmlogdmgm  24467  lgamgulmlem2  24473  lgamgulmlem3  24474  lgamgulmlem5  24476  lgambdd  24480  lgamucov  24481  wilthlem1  24511  wilth  24514  ftalem3  24518  efnnfsumcl  24546  isppw  24557  efchtdvds  24602  sqff1o  24625  fsumdvdsdiaglem  24626  dvdsppwf1o  24629  dvdsflf1o  24630  musum  24634  muinv  24636  dvdsmulf1o  24637  fsumvma2  24656  vmasum  24658  chpval2  24660  chpchtsum  24661  chpub  24662  mersenne  24669  perfect1  24670  bposlem1  24726  lgsfle1  24748  lgsle1  24754  lgsdirprm  24773  lgsne0  24777  lgseisenlem3  24819  lgseisenlem4  24820  lgsquadlem1  24822  lgsquadlem2  24823  2sqblem  24873  chebbnd1lem1  24875  chebbnd1  24878  chtppilim  24881  chpchtlim  24885  chpo1ub  24886  rplogsumlem2  24891  rpvmasumlem  24893  dchrmusumlema  24899  dchrvmasumlem1  24901  dchrisum0flblem2  24915  dchrisum0lema  24920  dchrisum0lem2a  24923  logsqvma  24948  selberg3lem2  24964  pntrsumo1  24971  pnt2  25019  ostthlem1  25033  ostth3  25044  axtgcgrrflx  25078  axtgcgrid  25079  axtgsegcon  25080  axtg5seg  25081  axtgbtwnid  25082  axtgpasch  25083  axtgcont1  25084  tglng  25159  axcontlem7  25568  axcontlem10  25571  umgrale  25616  usgraedg2  25670  usgraexmpledg  25698  clwlkfclwwlk1hashn  26134  eupatrl  26261  ablocom  26555  phpar2  26868  cbncms  26911  hlph  26935  hcaucvg  27233  hlimconvi  27238  shaddcl  27264  shmulcl  27265  chlimi  27281  chcompl  27289  choc1  27376  nmopre  27919  cnopc  27962  lnopl  27963  unop  27964  hmop  27971  cnfnc  27979  lnfnl  27980  nlelshi  28109  cnlnadjlem5  28120  elpjidm  28233  mdslle1i  28366  mdslle2i  28367  atcv0  28391  chpssati  28412  fovcld  28626  aciunf1lem  28650  padct  28691  ssnnssfz  28743  ressprs  28792  oduprs  28793  resspos  28796  resstos  28797  tleile  28798  ogrpinvOLD  28852  ogrpinv0le  28853  ogrpsub  28854  ogrpaddlt  28855  isarchi3  28878  archirng  28879  archirngz  28880  archiabllem1a  28882  archiabllem1b  28883  archiabllem2a  28885  archiabllem2c  28886  archiabllem2b  28887  archiabl  28889  orngsqr  28941  ornglmulle  28942  orngrmulle  28943  ofldtos  28948  ofldlt1  28950  ofldchr  28951  suborng  28952  subofld  28953  isarchiofld  28954  nn0omnd  28978  madjusmdetlem4  29030  qtophaus  29037  crefi  29048  cmpcref  29051  cmppcmp  29059  pcmplfin  29061  tpr2rico  29092  rge0scvg  29129  zrhunitpreima  29156  qqhrhm  29167  esummono  29249  gsumesum  29254  esumrnmpt2  29263  esumpinfval  29268  esumpcvgval  29273  esumpmono  29274  0elsiga  29310  sigaclcu  29313  issgon  29319  inelpisys  29350  ldsysgenld  29356  ldgenpisyslem1  29359  sxuni  29389  isrnmeas  29396  measvuni  29410  measssd  29411  ddemeas  29432  imambfm  29457  elmbfmvol2  29462  dya2icoseg2  29473  omssubaddlem  29494  omssubadd  29495  carsgsigalem  29510  pmeasmono  29519  sibfinima  29534  oddpwdc  29549  oddpwdcv  29550  eulerpartlemf  29565  eulerpartlemt  29566  eulerpartlemr  29569  eulerpartlemgvv  29571  eulerpartlemgs2  29575  sseqf  29587  fiblem  29593  probtot  29607  ballotlem4  29693  ballotlem5  29694  ballotlemfrc  29721  ballotlemirc  29726  ballotth  29732  bnj642  29878  bnj643  29879  bnj645  29880  bnj707  29885  bnj1379  29961  bnj1538  29985  bnj110  29988  bnj93  29993  bnj906  30060  bnj1006  30089  bnj1110  30110  bnj1121  30113  bnj1172  30129  bnj1204  30140  bnj1321  30155  bnj1364  30156  bnj1398  30162  bnj1450  30178  bnj1312  30186  bnj1501  30195  bnj1523  30199  subfacp1lem3  30224  subfacp1lem5  30226  pconcn  30266  sconpht  30271  conpcon  30277  cvmcov  30305  cvmliftlem1  30327  cvmliftlem10  30336  cvmlift2lem11  30355  cvmlift2lem12  30356  msubff1  30513  mvhf1  30516  mthmpps  30539  mclspps  30541  fundmpss  30716  tfisg  30766  frinsg  30792  frrlem5  30834  sltval2  30859  txpss3v  30961  pprodss4v  30967  fnetg  31316  neibastop1  31330  filnetlem3  31351  onint1  31424  bj-elid2  32059  icorempt2  32171  wl-nfeqfb  32298  phpreu  32359  fin2solem  32361  fin2so  32362  lindsenlbs  32370  matunitlindflem1  32371  matunitlindflem2  32372  matunitlindf  32373  ptrest  32374  poimirlem1  32376  poimirlem2  32377  poimirlem3  32378  poimirlem4  32379  poimirlem5  32380  poimirlem6  32381  poimirlem7  32382  poimirlem8  32383  poimirlem9  32384  poimirlem10  32385  poimirlem11  32386  poimirlem12  32387  poimirlem13  32388  poimirlem14  32389  poimirlem15  32390  poimirlem16  32391  poimirlem17  32392  poimirlem18  32393  poimirlem19  32394  poimirlem20  32395  poimirlem21  32396  poimirlem22  32397  poimirlem23  32398  poimirlem24  32399  poimirlem26  32401  poimirlem27  32402  poimirlem29  32404  poimirlem31  32406  mblfinlem2  32413  dvtan  32426  itg2gt0cn  32431  ftc1anclem7  32457  ftc1anclem8  32458  ftc1anc  32459  cover2  32474  indexa  32494  istotbnd3  32536  sstotbnd2  32539  sstotbnd  32540  totbndss  32542  equivtotbnd  32543  isbnd3  32549  totbndbnd  32554  equivbnd  32555  prdsbnd  32558  prdstotbnd  32559  heibor  32586  mndoisexid  32634  zrdivrng  32718  crngocom  32766  isfld2  32770  dmncrng  32821  prter2  32980  toycom  33074  lsateln0  33096  lpssat  33114  lssat  33117  oposlem  33283  olop  33315  omllaw  33344  cvlexch1  33429  dihpN  35439  mapdordlem2  35740  nacsfg  36082  nacsfix  36089  mzpindd  36123  diophrw  36136  diophrex  36153  rexzrexnn0  36182  pell1234qrdich  36239  rmspecsqrtnqOLD  36285  rmspecnonsq  36286  rmspecfund  36288  rmspecpos  36295  monotoddzzfi  36321  ltrmxnn0  36330  rmxnn  36332  jm2.23  36377  jm3.1lem2  36399  dnnumch3  36431  lnmlssfg  36464  lnmlmic  36472  lnrlnm  36498  lnr2i  36501  lpirlnr  36502  hbtlem6  36514  hbt  36515  mnccoe  36523  cntzsdrg  36587  idomrootle  36588  proot1mul  36592  proot1hash  36593  deg1mhm  36600  ntrneifv2  37194  radcnvrat  37331  binomcxplemdvbinom  37370  binomcxplemcvg  37371  binomcxplemnotnn0  37373  ordelordALT  37564  2uasbanh  37594  ordelordALTVD  37921  elixpconstg  38090  foelrnf  38164  disjinfi  38171  sumnnodd  38494  stoweidlem7  38697  stoweidlem14  38704  stoweidlem16  38706  stoweidlem24  38714  stoweidlem31  38721  stoweidlem54  38744  wallispilem3  38757  fourierdlem42  38839  fourierdlem48  38844  fourierdlem51  38847  fourierdlem64  38860  fourierdlem76  38872  fourierdlem79  38875  fourierdlem81  38877  fourierdlem87  38883  etransclem28  38952  etransclem32  38956  sge0fodjrnlem  39106  hoidmvlelem3  39284  preimagelt  39386  preimalegt  39387  pimrecltpos  39393  pimrecltneg  39407  issmflem  39410  smfaddlem1  39446  2reu1  39632  nfunsnafv  39669  faovcl  39727  evendiv2z  39881  oddp1div2z  39882  2dvdseven  39902  2ndvdsodd  39903  perfectALTVlem1  39962  upgrle  40311  umgredg2  40320  lfgredgge2  40344  usgredg2ALT  40415  usgr1vr  40476  usgrexmpledg  40481  upgrres1  40527  fusgrvtxfi  40533  nbfusgrlevtxm1  40600  nbfusgrlevtxm2  40601  cusgrcplgr  40637  vdumgr0  40690  trlres  40903  usgr2pth  40965  umgrn1cycl  41005  clwlksfclwwlk1hashn  41261  clintopcllaw  41632  0ringbas  41656  rnghmmgmhm  41679  uzlidlring  41714  rnghmsubcsetclem1  41762  rngccatidALTV  41776  zrinitorngc  41787  zrtermorngc  41788  rhmsubcsetclem1  41808  funcringcsetcALTV2lem7  41829  ringccatidALTV  41839  funcringcsetclem7ALTV  41852  irinitoringc  41856  zrtermoringc  41857  fldhmsubc  41871  fldhmsubcALTV  41890  ssnn0ssfz  41915  el0ldepsnzr  42045  regt1loggt0  42123  elbigodm  42142  fllogbd  42147
  Copyright terms: Public domain W3C validator