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

Theorem simprbi 480
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 479 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  xornan  1469  sb1  1880  eumo  2498  reurmo  3154  pssne  3687  pssn2lp  3692  ssnpss  3694  eldifn  3717  elinel2  3784  rabsnt  4243  eldifsni  4296  unimax  4446  ssintub  4467  moop2  4936  pwssun  4990  weso  5075  opelxp2  5121  wfisg  5684  ordwe  5705  funmo  5873  funopg  5890  funun  5900  fununi  5932  funimaexg  5943  fndm  5958  frn  6020  f1ss  6073  f1ssr  6074  f1ssres  6075  forn  6085  f1f1orn  6115  f1orescnv  6119  f1imacnv  6120  funcocnv2  6128  dffv2  6238  exfo  6343  foelrn  6344  isorel  6541  isoini2  6554  f1ofveu  6610  fovcl  6730  f1opw  6854  onminesb  6960  onminsb  6961  tfis  7016  limomss  7032  nnlim  7040  ssnlim  7045  curry1  7229  curry2  7232  f1o2ndf1  7245  fnwelem  7252  ressuppss  7274  mpt2xopn0yelv  7299  wfrlem5  7379  tz7.48lem  7496  dif20el  7545  oeordi  7627  oeeulem  7641  oeeui  7642  nnawordex  7677  swoer  7732  erdisj  7754  eceqoveq  7813  mapsnconst  7863  resixpfo  7906  boxcutc  7911  sdomnen  7944  en0  7979  en1  7983  domunsncan  8020  fodomr  8071  phplem4  8102  php3  8106  unxpdomlem3  8126  fineqvlem  8134  f1opwfi  8230  fsuppcolem  8266  fsuppco  8267  mapfienlem1  8270  mapfienlem2  8271  supub  8325  suplub  8326  ordtypelem2  8384  ordtypelem3  8385  ordtypelem6  8388  ordtypelem7  8389  wemapso2lem  8417  wdom2d  8445  brwdom3  8447  ixpiunwdom  8456  inf3lem2  8486  inf3lem6  8490  oancom  8508  infdifsn  8514  cantnfp1lem3  8537  cantnflem3  8548  cantnflem4  8549  oef1o  8555  cnfcom3  8561  tctr  8576  tz9.12lem3  8612  scottex  8708  cardid2  8739  infxpenlem  8796  acni3  8830  cardaleph  8872  iscard3  8876  dfac5lem4  8909  dfac5lem5  8910  kmlem1  8932  cofsmo  9051  fin4en1  9091  enfin2i  9103  fin23lem28  9122  fin23lem38  9131  isf32lem6  9140  enfin1ai  9166  isfin1-3  9168  hsmexlem2  9209  hsmexlem4  9211  domtriomlem  9224  axdc2lem  9230  axdc3lem2  9233  ac6num  9261  zorn2lem2  9279  brdom3  9310  alephval2  9354  alephreg  9364  pwcfsdom  9365  smobeth  9368  fpwwe2lem6  9417  fpwwe2lem13  9424  canthp1lem2  9435  pwfseqlem3  9442  hargch  9455  winalim2  9478  gchina  9481  inar1  9557  0npi  9664  mulclpi  9675  mulcanpi  9682  nlt1pi  9688  nqereu  9711  prcdnq  9775  prnmax  9777  ltresr2  9922  axrnegex  9943  axpre-sup  9950  eluz2gt1  11720  1nuz2  11724  zsupss  11737  rpgt0  11804  ixxss1  12151  ixxss2  12152  ixxss12  12153  lbioo  12164  ubioo  12165  iccss2  12202  iccssico2  12205  elfzuz3  12297  uzdisj  12370  nn0disj  12412  serge0  12811  expge0  12852  expge1  12853  expaddzlem  12859  hashrabsn1  13119  hashfun  13180  cshinj  13510  relexpuzrel  13742  shftfn  13763  sqrlem6  13938  rlimss  14183  lo1dm  14200  o1dm  14211  rlimrege0  14260  fsumf1o  14403  fsumge0  14473  incexc2  14514  supcvg  14532  fprodf1o  14620  divalglem9  15067  bitsfzolem  15099  bitsinv2  15108  bitsf1ocnv  15109  bitsf1  15111  gcdcllem1  15164  bezout  15203  prmind2  15341  nprm  15344  sqnprm  15357  dvdsprm  15358  isprm5  15362  coprm  15366  phibndlem  15418  dfphi2  15422  phimullem  15427  phisum  15438  pclem  15486  pcpre1  15490  pcidlem  15519  expnprm  15549  prmreclem1  15563  prmreclem2  15564  prmreclem5  15567  1arith  15574  4sqlem18  15609  vdwnnlem3  15644  ramtlecl  15647  rami  15662  0ram  15667  ramub1lem1  15673  prmgaplem5  15702  firest  16033  acsfiel  16255  isacs1i  16258  catlid  16284  catrid  16285  fullfo  16512  fthf1  16517  fthoppc  16523  invfuc  16574  prslem  16871  posi  16890  dlatmjdi  17134  pslem  17146  tsrlin  17159  cnvtsr  17162  tsrdir  17178  mndid  17243  mhmf  17280  mhmlin  17282  mhm0  17283  mrcmndind  17306  grpinvex  17372  grplinv  17408  mulgz  17508  mulgdirlem  17512  mulgdir  17513  mulgass  17519  nsgbi  17565  nmzbi  17574  ghmf  17604  ghmlin  17605  conjnsg  17636  gimf1o  17645  gagrpid  17667  gaf  17668  gaass  17670  psgnunilem5  17854  odid  17897  odf1o2  17928  gexid  17936  sylow1lem4  17956  odcau  17959  pj1id  18052  efgredeu  18105  ablcmn  18139  cmncom  18149  mulgdi  18172  gexexlem  18195  torsubg  18197  cyggenod2  18227  cygctb  18233  ghmcyg  18237  dprdf1o  18371  dprd2dlem1  18380  dprd2da  18381  ablfacrplem  18404  ablfaclem2  18425  ablfac2  18428  crngmgp  18495  rhmmhm  18662  rhmghm  18665  drngunit  18692  drngmgp  18699  drngid  18701  subrgss  18721  subrg1cl  18728  issubdrg  18745  abvge0  18765  srngcnv  18793  lmhmlin  18975  lmimf1o  19003  lvecdrng  19045  lspsolvlem  19082  islbs3  19095  lbsextlem3  19100  2idlcpbl  19174  nzrnz  19200  opprnzr  19205  rrgeq0i  19229  domneq0  19237  domnrrg  19240  drngdomn  19243  fldidom  19245  assalem  19256  mplsubrglem  19379  mplcoe1  19405  mplbas2  19410  opsrtoslem2  19425  mplelsfi  19431  coe1mul2  19579  zringunit  19776  prmirredlem  19781  znidomb  19850  cygzn  19859  psgndiflemB  19886  pjf  19997  frlmsslsp  20075  frlmlbs  20076  f1lindf  20101  pmatcoe1fsupp  20446  toponuni  20659  tpsuni  20680  clsval2  20794  mretopd  20836  neips  20857  neiptoptop  20875  neiptopnei  20876  perflp  20898  perfi  20899  restfpw  20923  cnf  20990  cnpf  20991  cnpimaex  21000  cnima  21009  t0sep  21068  t1ficld  21071  hausnei  21072  pnrmcld  21086  cnrmi  21104  cmpcov  21132  discmp  21141  tgcmp  21144  uncmp  21146  hauscmplem  21149  cmpfi  21151  connclo  21158  1stcclb  21187  2ndcdisj  21199  llyi  21217  nllyi  21218  ptpjpre1  21314  ptpjcn  21354  ptpjopn  21355  ptclsg  21358  dfac14  21361  txdis1cn  21378  pthaus  21381  hauseqlcld  21389  txkgen  21395  xkococn  21403  txconn  21432  hmeocnvcn  21504  fbssfi  21581  filss  21597  ufilss  21649  uffixfr  21667  flimneiss  21710  flimelbas  21712  fclscf  21769  flimfnfcls  21772  alexsublem  21788  alexsubb  21790  alexsubALT  21795  ptcmplem2  21797  ptcmplem3  21798  ptcmplem4  21799  tmdgsum2  21840  ghmcnp  21858  tgpt0  21862  qustgplem  21864  tsmsfbas  21871  tsmslem1  21872  tsmsgsum  21882  tsmssubm  21886  tsmsres  21887  tsmsf1o  21888  tsmsmhm  21889  tsmsadd  21890  tsmsxplem1  21896  tsmsxplem2  21897  tsmsxp  21898  istdrg2  21921  vscacn  21929  tvctdrg  21936  uspreg  22018  ucncn  22029  neipcfilu  22040  cuspcvg  22045  psmetxrge0  22058  isxmet2d  22072  prdsxmetlem  22113  imasdsf1olem  22118  xmstopn  22196  mstopn  22197  stdbdxmet  22260  prdsxmslem2  22274  nrgabv  22405  nmvs  22420  nvclvec  22441  nmoge0  22465  nghmcl  22471  nmoi  22472  nghmghm  22478  nmhmlmhm  22493  nmhmnghm  22494  icccmp  22568  xrge0gsumle  22576  xrge0tsms  22577  metds0  22593  metdstri  22594  metdsre  22596  metdseq0  22597  metdscnlem  22598  metnrmlem1a  22601  icopnfcnv  22681  xrhmeo  22685  pcoval1  22753  cvslvec  22865  cvsunit  22871  cphreccllem  22918  cmetcvg  23023  lmle  23039  cmscmet  23083  cmetcusp1  23089  hlcph  23100  minveclem4  23143  ivthlem3  23162  ovolmge0  23185  ovolicc1  23224  ovolicc2lem3  23227  ovolicc2lem5  23229  mblsplit  23240  dyadmbl  23308  mbfdm  23335  mbfadd  23368  mbfsub  23369  i1ff  23383  i1frn  23384  i1fima2  23386  mbfmul  23433  itg2monolem1  23457  bddmulibl  23545  dvnres  23634  c1liplem1  23697  c1lip2  23699  dvge0  23707  lhop1lem  23714  itgsubstlem  23749  fta1glem1  23863  fta1glem2  23864  fta1b  23867  plyf  23892  plypf1  23906  plyadd  23911  plymul  23912  coeeu  23919  dgrlem  23923  coeid  23932  elqaalem3  24014  aareccl  24019  eff1olem  24232  relogf1o  24251  logdmn0  24320  logcnlem2  24323  logcnlem3  24324  dvloglem  24328  efopnlem1  24336  efopnlem2  24337  logtayl2  24342  cxpcn3lem  24422  cxpcn3  24423  atandmneg  24567  atandmcj  24570  efiatan2  24578  cosatan  24582  cosatanne0  24583  dvatan  24596  areage0  24624  cxp2lim  24637  jensenlem2  24648  jensen  24649  eldmgm  24682  dmgmaddn0  24683  dmlogdmgm  24684  lgamgulmlem2  24690  lgamgulmlem3  24691  lgamgulmlem5  24693  lgambdd  24697  lgamucov  24698  wilthlem1  24728  wilth  24731  ftalem3  24735  efnnfsumcl  24763  isppw  24774  efchtdvds  24819  sqff1o  24842  fsumdvdsdiaglem  24843  dvdsppwf1o  24846  dvdsflf1o  24847  musum  24851  muinv  24853  dvdsmulf1o  24854  fsumvma2  24873  vmasum  24875  chpval2  24877  chpchtsum  24878  chpub  24879  mersenne  24886  perfect1  24887  bposlem1  24943  lgsfle1  24965  lgsle1  24971  lgsdirprm  24990  lgsne0  24994  lgseisenlem3  25036  lgseisenlem4  25037  lgsquadlem1  25039  lgsquadlem2  25040  2sqblem  25090  chebbnd1lem1  25092  chebbnd1  25095  chtppilim  25098  chpchtlim  25102  chpo1ub  25103  rplogsumlem2  25108  rpvmasumlem  25110  dchrmusumlema  25116  dchrvmasumlem1  25118  dchrisum0flblem2  25132  dchrisum0lema  25137  dchrisum0lem2a  25140  logsqvma  25165  selberg3lem2  25181  pntrsumo1  25188  pnt2  25236  ostthlem1  25250  ostth3  25261  axtgcgrrflx  25295  axtgcgrid  25296  axtgsegcon  25297  axtg5seg  25298  axtgbtwnid  25299  axtgpasch  25300  axtgcont1  25301  tglng  25375  axcontlem7  25784  axcontlem10  25787  upgrle  25915  umgredg2  25924  lfgredgge2  25948  usgredg2ALT  26012  usgr1vr  26074  usgrexmpledg  26081  upgrres1  26127  fusgrvtxfi  26133  nbfusgrlevtxm1  26200  nbfusgrlevtxm2  26201  cusgrcplgr  26237  vdumgr0  26296  trlres  26500  usgr2pth  26563  umgrn1cycl  26602  clwlksfclwwlk1hashn  26859  ablocom  27290  phpar2  27566  cbncms  27609  hlph  27633  hcaucvg  27931  hlimconvi  27936  shaddcl  27962  shmulcl  27963  chlimi  27979  chcompl  27987  choc1  28074  nmopre  28617  cnopc  28660  lnopl  28661  unop  28662  hmop  28669  cnfnc  28677  lnfnl  28678  nlelshi  28807  cnlnadjlem5  28818  elpjidm  28931  mdslle1i  29064  mdslle2i  29065  atcv0  29089  chpssati  29110  fovcld  29323  aciunf1lem  29345  padct  29381  ssnnssfz  29432  ressprs  29482  oduprs  29483  resspos  29486  resstos  29487  tleile  29488  ogrpinvOLD  29542  ogrpinv0le  29543  ogrpsub  29544  ogrpaddlt  29545  isarchi3  29568  archirng  29569  archirngz  29570  archiabllem1a  29572  archiabllem1b  29573  archiabllem2a  29575  archiabllem2c  29576  archiabllem2b  29577  archiabl  29579  orngsqr  29631  ornglmulle  29632  orngrmulle  29633  ofldtos  29638  ofldlt1  29640  ofldchr  29641  suborng  29642  subofld  29643  isarchiofld  29644  nn0omnd  29668  madjusmdetlem4  29720  qtophaus  29727  crefi  29738  cmpcref  29741  cmppcmp  29749  pcmplfin  29751  tpr2rico  29782  rge0scvg  29819  zrhunitpreima  29846  qqhrhm  29857  esummono  29939  gsumesum  29944  esumrnmpt2  29953  esumpinfval  29958  esumpcvgval  29963  esumpmono  29964  0elsiga  30000  sigaclcu  30003  issgon  30009  inelpisys  30040  ldsysgenld  30046  ldgenpisyslem1  30049  sxuni  30079  isrnmeas  30086  measvuni  30100  measssd  30101  ddemeas  30122  imambfm  30147  elmbfmvol2  30152  dya2icoseg2  30163  omssubaddlem  30184  omssubadd  30185  carsgsigalem  30200  pmeasmono  30209  sibfinima  30224  oddpwdc  30239  oddpwdcv  30240  eulerpartlemf  30255  eulerpartlemt  30256  eulerpartlemr  30259  eulerpartlemgvv  30261  eulerpartlemgs2  30265  sseqf  30277  fiblem  30283  probtot  30297  ballotlem4  30383  ballotlem5  30384  ballotlemfrc  30411  ballotlemirc  30416  ballotth  30422  bnj642  30579  bnj643  30580  bnj645  30581  bnj707  30586  bnj1379  30662  bnj1538  30686  bnj110  30689  bnj93  30694  bnj906  30761  bnj1006  30790  bnj1110  30811  bnj1121  30814  bnj1204  30841  bnj1321  30856  bnj1364  30857  bnj1398  30863  bnj1450  30879  bnj1312  30887  bnj1501  30896  bnj1523  30900  subfacp1lem3  30925  subfacp1lem5  30927  pconncn  30967  connpconn  30978  cvmcov  31006  cvmliftlem1  31028  cvmliftlem10  31037  cvmlift2lem11  31056  cvmlift2lem12  31057  msubff1  31214  mvhf1  31217  mthmpps  31240  mclspps  31242  fundmpss  31421  tfisg  31470  frinsg  31496  frrlem5  31538  sltval2  31563  txpss3v  31680  pprodss4v  31686  fnetg  32035  neibastop1  32049  filnetlem3  32070  onint1  32143  bj-elid2  32758  icorempt2  32870  wl-nfeqfb  32994  phpreu  33064  fin2solem  33066  fin2so  33067  lindsenlbs  33075  matunitlindflem1  33076  matunitlindflem2  33077  matunitlindf  33078  ptrest  33079  poimirlem1  33081  poimirlem2  33082  poimirlem3  33083  poimirlem4  33084  poimirlem5  33085  poimirlem6  33086  poimirlem7  33087  poimirlem8  33088  poimirlem9  33089  poimirlem10  33090  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem14  33094  poimirlem15  33095  poimirlem16  33096  poimirlem17  33097  poimirlem18  33098  poimirlem19  33099  poimirlem20  33100  poimirlem21  33101  poimirlem22  33102  poimirlem23  33103  poimirlem24  33104  poimirlem26  33106  poimirlem27  33107  poimirlem29  33109  poimirlem31  33111  mblfinlem2  33118  dvtan  33131  itg2gt0cn  33136  ftc1anclem7  33162  ftc1anclem8  33163  ftc1anc  33164  cover2  33179  indexa  33199  istotbnd3  33241  sstotbnd2  33244  sstotbnd  33245  totbndss  33247  equivtotbnd  33248  isbnd3  33254  totbndbnd  33259  equivbnd  33260  prdsbnd  33263  prdstotbnd  33264  heibor  33291  zrdivrng  33423  crngocom  33471  isfld2  33475  dmncrng  33526  prter2  33685  toycom  33779  lsateln0  33801  lpssat  33819  lssat  33822  oposlem  33988  olop  34020  omllaw  34049  cvlexch1  34134  dihpN  36144  mapdordlem2  36445  nacsfg  36787  nacsfix  36794  mzpindd  36828  diophrw  36841  diophrex  36858  rexzrexnn0  36887  pell1234qrdich  36944  rmspecsqrtnqOLD  36990  rmspecnonsq  36991  rmspecfund  36993  rmspecpos  37000  monotoddzzfi  37026  ltrmxnn0  37035  rmxnn  37037  jm2.23  37082  jm3.1lem2  37104  dnnumch3  37136  lnmlssfg  37169  lnmlmic  37177  lnrlnm  37203  lnr2i  37206  lpirlnr  37207  hbtlem6  37219  hbt  37220  mnccoe  37228  cntzsdrg  37292  idomrootle  37293  proot1mul  37297  proot1hash  37298  deg1mhm  37305  ntrneifv2  37899  radcnvrat  38034  binomcxplemdvbinom  38073  binomcxplemcvg  38074  binomcxplemnotnn0  38076  ordelordALT  38268  2uasbanh  38298  ordelordALTVD  38625  elixpconstg  38788  rabidim2  38806  foelrnf  38882  disjinfi  38889  sumnnodd  39298  stoweidlem7  39561  stoweidlem14  39568  stoweidlem16  39570  stoweidlem24  39578  stoweidlem31  39585  stoweidlem54  39608  wallispilem3  39621  fourierdlem42  39703  fourierdlem48  39708  fourierdlem51  39711  fourierdlem64  39724  fourierdlem76  39736  fourierdlem79  39739  fourierdlem81  39741  fourierdlem87  39747  etransclem28  39816  etransclem32  39820  sge0fodjrnlem  39970  hoidmvlelem3  40148  preimagelt  40249  preimalegt  40250  pimrecltpos  40256  pimrecltneg  40270  issmflem  40273  smfaddlem1  40308  smfsuplem1  40354  smfsuplem3  40356  smflimsuplem7  40369  nfunsnafv  40556  faovcl  40614  evendiv2z  40874  oddp1div2z  40875  2dvdseven  40895  2ndvdsodd  40896  perfectALTVlem1  40955  sprel  41052  clintopcllaw  41165  0ringbas  41189  rnghmmgmhm  41212  uzlidlring  41247  rnghmsubcsetclem1  41293  rngccatidALTV  41307  zrinitorngc  41318  zrtermorngc  41319  rhmsubcsetclem1  41339  funcringcsetcALTV2lem7  41360  ringccatidALTV  41370  funcringcsetclem7ALTV  41383  irinitoringc  41387  zrtermoringc  41388  fldhmsubc  41402  fldhmsubcALTV  41420  ssnn0ssfz  41445  el0ldepsnzr  41574  regt1loggt0  41652  elbigodm  41671  fllogbd  41676  elsetrecslem  41767
  Copyright terms: Public domain W3C validator