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

Theorem simprbi 486
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 207 . 2 (𝜑 → (𝜓𝜒))
32simprd 485 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 385
This theorem is referenced by:  simplbiim  495  xornan  1626  sb1  2062  eumoOLD  2659  reurmo  3346  pssne  3895  pssn2lp  3900  ssnpss  3902  eldifn  3926  elinel2  3993  rabsnt  4451  eldifsni  4506  unimax  4660  ssintub  4680  moop2  5149  pwssun  5209  weso  5296  opelxp2  5345  wfisg  5922  ordwe  5943  funmo  6111  funopg  6129  funun  6140  fununi  6169  funimaexg  6180  fndm  6195  frn  6256  f1ss  6315  f1ssr  6316  f1ssres  6317  forn  6328  f1f1orn  6358  f1orescnv  6362  f1imacnv  6363  funcocnv2  6371  dffv2  6486  exfo  6593  foelrn  6594  isorel  6794  isoini2  6807  f1ofveu  6863  fovcl  6989  f1opw  7113  onminesb  7222  onminsb  7223  tfis  7278  limomss  7294  nnlim  7302  ssnlim  7307  curry1  7497  curry2  7500  f1o2ndf1  7513  fnwelem  7520  ressuppss  7542  mpt2xopn0yelv  7568  wfrlem5  7649  tz7.48lem  7766  dif20el  7816  oeordi  7898  oeeulem  7912  oeeui  7913  nnawordex  7948  swoer  8003  erdisj  8023  eceqoveq  8082  mapsnconst  8134  resixpfo  8177  boxcutc  8182  sdomnen  8215  en0  8249  en1  8253  domunsncan  8293  fodomr  8344  phplem4  8375  php3  8379  unxpdomlem3  8399  fineqvlem  8407  f1opwfi  8503  fsuppcolem  8539  fsuppco  8540  mapfienlem1  8543  mapfienlem2  8544  supub  8598  suplub  8599  ordtypelem2  8657  ordtypelem3  8658  ordtypelem6  8661  ordtypelem7  8662  wemapso2lem  8690  wdom2d  8718  brwdom3  8720  ixpiunwdom  8729  inf3lem2  8767  inf3lem6  8771  oancom  8789  infdifsn  8795  cantnfp1lem3  8818  cantnflem3  8829  cantnflem4  8830  oef1o  8836  cnfcom3  8842  tctr  8857  tz9.12lem3  8893  scottex  8989  cardid2  9056  infxpenlem  9113  acni3  9147  cardaleph  9189  iscard3  9193  dfac5lem4  9226  dfac5lem5  9227  kmlem1  9251  cofsmo  9370  fin4en1  9410  enfin2i  9422  fin23lem28  9441  fin23lem38  9450  isf32lem6  9459  enfin1ai  9485  isfin1-3  9487  hsmexlem2  9528  hsmexlem4  9530  domtriomlem  9543  axdc2lem  9549  axdc3lem2  9552  ac6num  9580  zorn2lem2  9598  brdom3  9629  alephval2  9673  alephreg  9683  pwcfsdom  9684  smobeth  9687  fpwwe2lem6  9736  fpwwe2lem13  9743  canthp1lem2  9754  pwfseqlem3  9761  hargch  9774  winalim2  9797  gchina  9800  inar1  9876  0npi  9983  mulclpi  9994  mulcanpi  10001  nlt1pi  10007  nqereu  10030  prcdnq  10094  prnmax  10096  ltresr2  10241  axrnegex  10262  axpre-sup  10269  eluz2gt1  11973  1nuz2  11977  zsupss  11990  rpgt0  12052  ixxss1  12405  ixxss2  12406  ixxss12  12407  lbioo  12418  ubioo  12419  iccss2  12456  iccssico2  12459  elfzuz3  12556  uzdisj  12630  nn0disj  12673  serge0  13072  expge0  13113  expge1  13114  expaddzlem  13120  hashrabsn1  13375  hashfun  13435  cshinj  13775  relexpuzrel  14009  shftfn  14030  sqrlem6  14205  rlimss  14450  lo1dm  14467  o1dm  14478  rlimrege0  14527  fsumf1o  14671  fsumge0  14743  incexc2  14786  supcvg  14804  fprodf1o  14891  divalglem9  15338  bitsfzolem  15369  bitsinv2  15378  bitsf1ocnv  15379  bitsf1  15381  gcdcllem1  15434  bezout  15473  prmind2  15610  nprm  15613  sqnprm  15625  dvdsprm  15626  isprm5  15630  coprm  15634  phibndlem  15686  dfphi2  15690  phimullem  15695  phisum  15706  pclem  15754  pcpre1  15758  pcidlem  15787  expnprm  15817  prmreclem1  15831  prmreclem2  15832  prmreclem5  15835  1arith  15842  4sqlem18  15877  vdwnnlem3  15912  ramtlecl  15915  rami  15930  0ram  15935  ramub1lem1  15941  prmgaplem5  15970  firest  16292  acsfiel  16513  isacs1i  16516  catlid  16542  catrid  16543  fullfo  16770  fthf1  16775  fthoppc  16781  invfuc  16832  prslem  17130  posi  17149  dlatmjdi  17393  pslem  17405  tsrlin  17418  cnvtsr  17421  tsrdir  17437  mndid  17502  mhmf  17539  mhmlin  17541  mhm0  17542  mrcmndind  17565  grpinvex  17631  grplinv  17667  mulgz  17766  mulgdirlem  17769  mulgdir  17770  mulgass  17775  nsgbi  17821  nmzbi  17830  ghmf  17860  ghmlin  17861  conjnsg  17892  gimf1o  17901  gagrpid  17922  gaf  17923  gaass  17925  psgnunilem5  18109  odid  18152  odf1o2  18183  gexid  18191  sylow1lem4  18211  odcau  18214  pj1id  18307  efgredeu  18360  ablcmn  18394  cmncom  18404  mulgdi  18427  gexexlem  18450  torsubg  18452  cyggenod2  18482  cygctb  18488  ghmcyg  18492  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  19236  lmimf1o  19264  lvecdrng  19306  lspsolvlem  19344  islbs3  19358  lbsextlem3  19363  2idlcpbl  19437  nzrnz  19463  opprnzr  19468  rrgeq0i  19492  domneq0  19500  domnrrg  19503  drngdomn  19506  fldidom  19508  assalem  19519  mplsubrglem  19642  mplcoe1  19668  mplbas2  19673  opsrtoslem2  19687  mplelsfi  19693  coe1mul2  19841  zringunit  20038  prmirredlem  20043  znidomb  20111  cygzn  20120  psgndiflemB  20148  pjf  20261  frlmsslsp  20339  frlmlbs  20340  f1lindf  20365  pmatcoe1fsupp  20713  toponuni  20926  tpsuni  20948  clsval2  21062  mretopd  21104  neips  21125  neiptoptop  21143  neiptopnei  21144  perflp  21166  perfi  21167  restfpw  21191  cnf  21258  cnpf  21259  cnpimaex  21268  cnima  21277  t0sep  21336  t1ficld  21339  hausnei  21340  pnrmcld  21354  cnrmi  21372  cmpcov  21400  discmp  21409  tgcmp  21412  uncmp  21414  hauscmplem  21417  cmpfi  21419  connclo  21426  1stcclb  21455  2ndcdisj  21467  llyi  21485  nllyi  21486  ptpjpre1  21582  ptpjcn  21622  ptpjopn  21623  ptclsg  21626  dfac14  21629  txdis1cn  21646  pthaus  21649  hauseqlcld  21657  txkgen  21663  xkococn  21671  txconn  21700  hmeocnvcn  21772  fbssfi  21848  filss  21864  ufilss  21916  uffixfr  21934  flimneiss  21977  flimelbas  21979  fclscf  22036  flimfnfcls  22039  alexsublem  22055  alexsubb  22057  alexsubALT  22062  ptcmplem2  22064  ptcmplem3  22065  ptcmplem4  22066  tmdgsum2  22107  ghmcnp  22125  tgpt0  22129  qustgplem  22131  tsmsfbas  22138  tsmslem1  22139  tsmsgsum  22149  tsmssubm  22153  tsmsres  22154  tsmsf1o  22155  tsmsmhm  22156  tsmsadd  22157  tsmsxplem1  22163  tsmsxplem2  22164  tsmsxp  22165  istdrg2  22188  vscacn  22196  tvctdrg  22203  uspreg  22285  ucncn  22296  neipcfilu  22307  cuspcvg  22312  psmetxrge0  22325  isxmet2d  22339  prdsxmetlem  22380  imasdsf1olem  22385  xmstopn  22463  mstopn  22464  stdbdxmet  22527  prdsxmslem2  22541  nrgabv  22672  nmvs  22687  nvclvec  22708  nmoge0  22732  nghmcl  22738  nmoi  22739  nghmghm  22745  nmhmlmhm  22760  nmhmnghm  22761  icccmp  22835  xrge0gsumle  22843  xrge0tsms  22844  metds0  22860  metdstri  22861  metdsre  22863  metdseq0  22864  metdscnlem  22865  metnrmlem1a  22868  icopnfcnv  22948  xrhmeo  22952  pcoval1  23019  cvslvec  23131  cvsunit  23137  cphreccllem  23184  cmetcvg  23289  lmle  23305  cmscmet  23349  cmetcusp1  23355  hlcph  23366  minveclem4  23409  ivthlem3  23428  ovolmge0  23452  ovolicc1  23491  ovolicc2lem3  23494  ovolicc2lem5  23496  mblsplit  23507  dyadmbl  23575  mbfdm  23601  mbfadd  23636  mbfsub  23637  i1ff  23651  i1frn  23652  i1fima2  23654  mbfmul  23701  itg2monolem1  23725  bddmulibl  23813  dvnres  23902  c1liplem1  23967  c1lip2  23969  dvge0  23977  lhop1lem  23984  itgsubstlem  24019  fta1glem1  24133  fta1glem2  24134  fta1b  24137  plyf  24162  plypf1  24176  plyadd  24181  plymul  24182  coeeu  24189  dgrlem  24193  coeid  24202  elqaalem3  24284  aareccl  24289  eff1olem  24503  relogf1o  24521  logdmn0  24594  logcnlem2  24597  logcnlem3  24598  dvloglem  24602  efopnlem1  24610  efopnlem2  24611  logtayl2  24616  cxpcn3lem  24696  cxpcn3  24697  atandmneg  24841  atandmcj  24844  efiatan2  24852  cosatan  24856  cosatanne0  24857  dvatan  24870  areage0  24898  cxp2lim  24911  jensenlem2  24922  jensen  24923  eldmgm  24956  dmgmaddn0  24957  dmlogdmgm  24958  lgamgulmlem2  24964  lgamgulmlem3  24965  lgamgulmlem5  24967  lgambdd  24971  lgamucov  24972  wilthlem1  25002  wilth  25005  ftalem3  25009  efnnfsumcl  25037  isppw  25048  efchtdvds  25093  sqff1o  25116  fsumdvdsdiaglem  25117  dvdsppwf1o  25120  dvdsflf1o  25121  musum  25125  muinv  25127  dvdsmulf1o  25128  fsumvma2  25147  vmasum  25149  chpval2  25151  chpchtsum  25152  chpub  25153  mersenne  25160  perfect1  25161  bposlem1  25217  lgsfle1  25239  lgsle1  25245  lgsdirprm  25264  lgsne0  25268  lgseisenlem3  25310  lgseisenlem4  25311  lgsquadlem1  25313  lgsquadlem2  25314  2sqblem  25364  chebbnd1lem1  25366  chebbnd1  25369  chtppilim  25372  chpchtlim  25376  chpo1ub  25377  rplogsumlem2  25382  rpvmasumlem  25384  dchrmusumlema  25390  dchrvmasumlem1  25392  dchrisum0flblem2  25406  dchrisum0lema  25411  dchrisum0lem2a  25414  logsqvma  25439  selberg3lem2  25455  pntrsumo1  25462  pnt2  25510  ostthlem1  25524  ostth3  25535  axtgcgrrflx  25569  axtgcgrid  25570  axtgsegcon  25571  axtg5seg  25572  axtgbtwnid  25573  axtgpasch  25574  axtgcont1  25575  tglng  25649  axcontlem7  26058  axcontlem10  26061  upgrle  26193  umgredg2  26203  lfgredgge2  26227  usgredg2ALT  26294  usgr1vr  26357  usgrexmpledg  26364  upgrres1  26415  fusgrvtxfi  26421  vtxnbuvtx  26505  cusgrcplgr  26538  vdumgr0  26598  vtxdgoddnumeven  26671  trlres  26819  usgr2pth  26882  umgrn1cycl  26922  clwwlknlen  27174  clwlksfclwwlk1hashnOLD  27227  clwwnonrepclwwnon  27516  2clwwlk2  27519  ablocom  27725  phpar2  28000  cbncms  28043  hlph  28067  hcaucvg  28365  hlimconvi  28370  shaddcl  28396  shmulcl  28397  chlimi  28413  chcompl  28421  choc1  28508  nmopre  29051  cnopc  29094  lnopl  29095  unop  29096  hmop  29103  cnfnc  29111  lnfnl  29112  nlelshi  29241  cnlnadjlem5  29252  elpjidm  29365  mdslle1i  29498  mdslle2i  29499  atcv0  29523  chpssati  29544  fovcld  29761  aciunf1lem  29783  padct  29818  ssnnssfz  29870  ressprs  29974  oduprs  29975  resspos  29978  resstos  29979  tleile  29980  ogrpinvOLD  30034  ogrpinv0le  30035  ogrpsub  30036  ogrpaddlt  30037  isarchi3  30060  archirng  30061  archirngz  30062  archiabllem1a  30064  archiabllem1b  30065  archiabllem2a  30067  archiabllem2c  30068  archiabllem2b  30069  archiabl  30071  orngsqr  30123  ornglmulle  30124  orngrmulle  30125  ofldtos  30130  ofldlt1  30132  ofldchr  30133  suborng  30134  subofld  30135  isarchiofld  30136  nn0omnd  30160  madjusmdetlem4  30215  qtophaus  30222  crefi  30233  cmpcref  30236  cmppcmp  30244  pcmplfin  30246  tpr2rico  30277  rge0scvg  30314  zrhunitpreima  30341  qqhrhm  30352  esummono  30435  gsumesum  30440  esumrnmpt2  30449  esumpinfval  30454  esumpcvgval  30459  esumpmono  30460  0elsiga  30496  sigaclcu  30499  issgon  30505  inelpisys  30536  ldsysgenld  30542  ldgenpisyslem1  30545  sxuni  30575  isrnmeas  30582  measvuni  30596  measssd  30597  ddemeas  30618  imambfm  30643  elmbfmvol2  30648  dya2icoseg2  30659  omssubaddlem  30680  omssubadd  30681  carsgsigalem  30696  pmeasmono  30705  sibfinima  30720  oddpwdc  30735  oddpwdcv  30736  eulerpartlemf  30751  eulerpartlemt  30752  eulerpartlemr  30755  eulerpartlemgvv  30757  eulerpartlemgs2  30761  fiblem  30779  probtot  30793  ballotlem4  30879  ballotlem5  30880  ballotlemfrc  30907  ballotlemirc  30912  ballotth  30918  hgt750lemb  31053  bnj642  31135  bnj643  31136  bnj645  31137  bnj707  31142  bnj1379  31218  bnj1538  31242  bnj110  31245  bnj93  31250  bnj906  31317  bnj1006  31346  bnj1110  31367  bnj1121  31370  bnj1204  31397  bnj1321  31412  bnj1364  31413  bnj1398  31419  bnj1450  31435  bnj1312  31443  bnj1501  31452  bnj1523  31456  subfacp1lem3  31481  subfacp1lem5  31483  pconncn  31523  connpconn  31534  cvmcov  31562  cvmliftlem1  31584  cvmliftlem10  31593  cvmlift2lem11  31612  cvmlift2lem12  31613  msubff1  31770  mvhf1  31773  mthmpps  31796  mclspps  31798  fundmpss  31980  tfisg  32030  frpoinsg  32056  frinsg  32060  frrlem5  32099  sltval2  32124  txpss3v  32300  pprodss4v  32306  fnetg  32655  neibastop1  32669  filnetlem3  32690  onint1  32759  bj-elid2  33396  icorempt2  33509  wl-nfeqfb  33631  phpreu  33700  fin2solem  33702  fin2so  33703  lindsenlbs  33711  matunitlindflem1  33712  matunitlindflem2  33713  matunitlindf  33714  ptrest  33715  poimirlem1  33717  poimirlem2  33718  poimirlem3  33719  poimirlem4  33720  poimirlem5  33721  poimirlem6  33722  poimirlem7  33723  poimirlem8  33724  poimirlem9  33725  poimirlem10  33726  poimirlem11  33727  poimirlem12  33728  poimirlem13  33729  poimirlem14  33730  poimirlem15  33731  poimirlem16  33732  poimirlem17  33733  poimirlem18  33734  poimirlem19  33735  poimirlem20  33736  poimirlem21  33737  poimirlem22  33738  poimirlem23  33739  poimirlem24  33740  poimirlem26  33742  poimirlem27  33743  poimirlem29  33745  poimirlem31  33747  mblfinlem2  33754  dvtan  33766  itg2gt0cn  33771  ftc1anclem7  33797  ftc1anclem8  33798  ftc1anc  33799  cover2  33814  indexa  33834  istotbnd3  33875  sstotbnd2  33878  sstotbnd  33879  totbndss  33881  equivtotbnd  33882  isbnd3  33888  totbndbnd  33893  equivbnd  33894  prdsbnd  33897  prdstotbnd  33898  heibor  33925  zrdivrng  34057  crngocom  34105  isfld2  34109  dmncrng  34160  xrnss3v  34441  prter2  34654  toycom  34747  lsateln0  34769  lpssat  34787  lssat  34790  oposlem  34956  olop  34988  omllaw  35017  cvlexch1  35102  dihpN  37111  mapdordlem2  37412  nacsfg  37764  nacsfix  37771  mzpindd  37805  diophrw  37818  diophrex  37835  rexzrexnn0  37864  pell1234qrdich  37921  rmspecnonsq  37967  rmspecfund  37969  rmspecpos  37976  monotoddzzfi  38002  ltrmxnn0  38011  rmxnn  38013  jm2.23  38058  jm3.1lem2  38080  dnnumch3  38112  lnmlssfg  38145  lnmlmic  38153  lnrlnm  38178  lnr2i  38181  lpirlnr  38182  hbtlem6  38194  hbt  38195  mnccoe  38203  cntzsdrg  38267  idomrootle  38268  proot1mul  38272  proot1hash  38273  deg1mhm  38280  ntrneifv2  38872  radcnvrat  39007  binomcxplemdvbinom  39046  binomcxplemcvg  39047  binomcxplemnotnn0  39049  ordelordALT  39239  2uasbanh  39269  ordelordALTVD  39591  elixpconstg  39753  rabidim2  39770  foelrnf  39856  disjinfi  39863  supminfxr2  40172  sumnnodd  40336  stoweidlem7  40697  stoweidlem14  40704  stoweidlem16  40706  stoweidlem24  40714  stoweidlem31  40721  stoweidlem54  40744  wallispilem3  40757  fourierdlem42  40839  fourierdlem48  40844  fourierdlem51  40847  fourierdlem64  40860  fourierdlem76  40872  fourierdlem79  40875  fourierdlem81  40877  fourierdlem87  40883  etransclem28  40952  etransclem32  40956  sge0fodjrnlem  41106  hoidmvlelem3  41287  preimagelt  41388  preimalegt  41389  pimrecltpos  41395  pimrecltneg  41409  issmflem  41412  smfaddlem1  41447  smfsuplem1  41493  smfsuplem3  41495  smflimsuplem7  41508  smfliminflem  41512  nfunsnafv  41725  faovcl  41783  tz6.12-2-afv2  41820  tz6.12i-afv2  41826  evendiv2z  42114  oddp1div2z  42115  2dvdseven  42135  2ndvdsodd  42136  perfectALTVlem1  42199  sbgoldbm  42241  sprel  42296  clintopcllaw  42409  0ringbas  42433  rnghmmgmhm  42456  uzlidlring  42491  rnghmsubcsetclem1  42537  rngccatidALTV  42551  zrinitorngc  42562  zrtermorngc  42563  rhmsubcsetclem1  42583  funcringcsetcALTV2lem7  42604  ringccatidALTV  42614  funcringcsetclem7ALTV  42627  irinitoringc  42631  zrtermoringc  42632  fldhmsubc  42646  fldhmsubcALTV  42664  ssnn0ssfz  42689  el0ldepsnzr  42818  regt1loggt0  42892  elbigodm  42911  fllogbd  42916  elsetrecslem  43007
  Copyright terms: Public domain W3C validator