MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplbi Unicode version

Theorem simplbi 446
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simplbi.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi  |-  ( ph  ->  ps )

Proof of Theorem simplbi
StepHypRef Expression
1 simplbi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpi 186 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simpld 445 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  3simpa  952  reurex  2756  eqimss  3232  pssss  3273  eldifi  3300  inss1  3391  ssunsn2  3775  pwssun  4301  sopo  4333  wefr  4385  ordtr  4408  opelxp1  4724  relop  4836  funmo  5273  funrel  5274  fnfun  5343  ffn  5391  f1f  5439  f1of1  5473  f1ofo  5481  isof1o  5824  eqopi  6158  1st2nd2  6161  reldmtpos  6244  swoer  6690  erdisj  6709  ecopover  6764  sdomdom  6891  inf3lemd  7330  mapfien  7401  cardprclem  7614  infxpenlem  7643  cardinfima  7726  dfac5lem4  7755  domtriomlem  8070  smobeth  8210  fpwwe2lem6  8259  fpwwe2lem7  8260  fpwwe2lem12  8265  fpwwe2lem13  8266  fpwwe2  8267  axrnegex  8786  axpre-sup  8793  eqlei  8944  zre  10030  nnssz  10045  supminf  10307  ixxss1  10676  ixxss2  10677  ixxss12  10678  lbioo  10689  ubioo  10690  iccss2  10722  elfzuz  10796  uzdisj  10858  splfv1  11472  sqrlem6  11735  rlimf  11977  lo1f  11994  lo1dm  11995  o1f  12005  o1dm  12006  fsumge0  12255  incexc2  12299  mertenslem2  12343  divalglem9  12602  bitsinv2  12636  bitsf1ocnv  12637  gcdcllem1  12692  prmnn  12763  prmind2  12771  nprm  12774  prmuz2  12778  isprm6  12790  exprmfct  12791  isprm5  12793  maxprmfct  12794  phibndlem  12840  phibnd  12841  dfphi2  12844  phimullem  12849  pclem  12893  pcprendvds2  12896  pcpre1  12897  expnprm  12952  prmreclem1  12965  1arith  12976  4sqlem15  13008  4sqlem16  13009  vdwlem5  13034  vdwlem6  13035  vdwlem8  13037  vdwlem9  13038  vdwlem11  13040  ramtlecl  13049  0ramcl  13072  firest  13339  acsmre  13556  posprs  14085  latpos  14157  dlatl  14300  pslem  14317  tsrlemax  14331  tsrps  14332  laps  14347  mndlem1  14373  grpmnd  14496  nsgsubg  14651  ghmgrp1  14687  ghmgrp2  14688  gimghm  14730  gagrp  14748  gaset  14749  efgredeu  15063  ablgrp  15096  cmnmnd  15106  cyggenod2  15174  cyggrp  15178  ablfac2  15326  crngrng  15353  dvdsrcl  15433  unitcl  15443  drngrng  15521  subrgrng  15550  subrgrcl  15552  srngrhm  15618  lmimlmhm  15819  lveclmod  15861  2idlcpbl  15988  divs1  15989  divsrhm  15991  lpirrng  16006  nzrrng  16015  domnnzr  16038  fldidom  16048  assalmod  16062  assarng  16063  assasca  16064  cygznlem1  16522  cygznlem3  16525  topontop  16666  tpstop  16679  clsval2  16789  mretopd  16831  perftop  16889  restfpw  16912  cntop1  16972  cntop2  16973  cnptop1  16974  cnptop2  16975  cnprcl  16977  t1ficld  17057  t0top  17059  t1top  17060  haustop  17061  regtop  17063  nrmtop  17066  cnrmtop  17067  pnrmnrm  17070  cmptop  17124  discmp  17127  tgcmp  17130  uncmp  17132  conndisj  17144  contop  17145  1stctop  17171  llytop  17200  nllytop  17201  txdis1cn  17331  hmeocn  17453  filfbas  17545  ufilfil  17601  flimtop  17662  flimfil  17666  alexsublem  17740  ptcmplem3  17750  tsmsfbas  17812  tsmslem1  17813  tsmsgsum  17823  tsmssubm  17827  tsmsres  17828  tsmsf1o  17829  tsmsmhm  17830  tsmsadd  17831  tsmsxplem1  17837  tsmsxplem2  17838  tsmsxp  17839  tlmtmd  17871  tlmlmod  17873  tlmtrg  17874  tvctlm  17881  isxmet2d  17894  metxmet  17901  xmstps  18001  msxms  18002  xmsxmet  18004  msmet  18005  stdbdxmet  18063  nrgngp  18175  nlmngp  18190  nlmlmod  18191  nlmnrg  18192  nvcnlm  18208  nmoi  18239  nghmrcl1  18243  nghmrcl2  18244  nmhmrcl1  18258  nmhmrcl2  18259  qdensere  18281  xrge0gsumle  18340  xrge0tsms  18341  metds0  18356  metdstri  18357  metdsre  18359  metdseq0  18360  metdscnlem  18361  metnrmlem1a  18364  metnrmlem1  18365  icopnfcnv  18442  icopnfhmeo  18443  cmetmet  18714  cmsms  18772  hlbn  18782  ovolicc1  18877  ovolicc2lem5  18882  mblss  18892  mbff  18984  mbfres  19001  mbfadd  19018  mbfsub  19019  i1fmbf  19032  mbfmul  19083  bddmulibl  19195  limcmpt  19235  dvcnvlem  19325  c1liplem1  19345  c1lip2  19347  fta1glem1  19553  fta1glem2  19554  fta1g  19555  fta1b  19557  ply1pid  19567  aacn  19699  ulmf2  19765  logdmnrp  19990  logdmss  19991  logcnlem2  19992  logcnlem3  19993  logcnlem4  19994  logcnlem5  19995  logcn  19996  dvloglem  19997  logf1o2  19999  efopnlem1  20005  logtayl2  20011  cxpcn  20087  cxpcn3lem  20089  cxpcn3  20090  resqrcn  20091  atandmneg  20204  atandmcj  20207  cosatan  20219  cosatanne0  20220  birthdaylem1  20248  areacl  20259  cxp2lim  20273  jensenlem2  20284  jensen  20285  wilth  20311  sqff1o  20422  dvdsdivcl  20423  fsumdvdsdiaglem  20425  dvdsflf1o  20429  muinv  20435  dvdsmulf1o  20436  mersenne  20468  bposlem3  20527  lgsqrlem1  20582  lgsqrlem2  20583  lgsqrlem3  20584  lgsqrlem4  20585  lgseisenlem3  20592  lgsquad2lem2  20600  2sqlem6  20610  chebbnd1  20623  chtppilim  20626  chpchtlim  20630  chpo1ub  20631  rplogsumlem1  20635  rplogsumlem2  20636  dchrmusumlema  20644  dchrvmasumiflem1  20652  dchrisum0flblem2  20660  dchrisum0lema  20665  dchrisum0lem2  20669  logsqvma  20693  selberg3lem2  20709  pntrsumo1  20716  selbergsb  20726  pnt2  20764  ostthlem2  20779  ostth2lem2  20785  ablogrpo  20953  smgrpismgm  21001  mndoissmgrp  21008  nmogtmnf  21350  bnnv  21447  hlobn  21469  hcauseq  21766  hlimseqi  21770  hlimveci  21771  shss  21791  sh0  21797  chsh  21806  lnopf  22441  bdopln  22443  nmopgtmnf  22450  hmopf  22456  lnfnf  22466  unopf1o  22498  elunop2  22595  elpjhmop  22767  stcltrlem1  22858  mdslle1i  22899  mdslle2i  22900  ballotlemfc0  23053  ballotlemfcc  23054  ballotlem5  23060  ballotlemscr  23079  ballotlemfg  23086  ballotlemfrc  23087  ballotlemfrceq  23089  ballotlemrinv0  23093  rabexgfGS  23173  ssnnssfz  23279  lmxrge0  23377  xrge0tsmsd  23384  esumpcvgval  23448  insiga  23500  brsiga  23516  measssd  23545  measinb2  23552  pwcntmeas  23556  mbfmbfm  23565  imambfm  23569  elmbfmvol2  23574  mbfmcnt  23575  domprobmeas  23615  cndprob01  23640  isrrvv  23648  dstrvprob  23674  subfacval3  23722  pcontop  23758  sconpcon  23760  cvmcn  23795  cvmliftlem10  23827  eupagra  23884  fundmpss  24124  predel  24185  sltres  24320  funpartfun  24483  axcontlem2  24595  axcontlem7  24600  axcontlem8  24601  axcontlem10  24603  outsideofcol  24758  fordisxex  24965  alneal1  25011  dfdir2  25302  dirpre  25304  isibg1a  26122  fnebas  26284  filnetlem3  26340  istotbnd3  26506  totbndmet  26507  sstotbnd2  26509  sstotbnd  26510  equivtotbnd  26513  bndmet  26516  totbndbnd  26524  prdstotbnd  26529  crngorngo  26636  prrngorngo  26687  divrngpr  26689  an3  26725  nacsacs  26795  eldiophelnn0  26854  jm2.17a  27058  jm2.17b  27059  jm2.17c  27060  jm2.27c  27111  jm3.1lem1  27121  jm3.1lem2  27122  jm3.1lem3  27123  lnmlmod  27188  lbslinds  27314  lnrrng  27327  mncply  27353  psgneu  27440  idomrootle  27522  idomodle  27523  hashgcdlem  27527  fnvinran  27696  cncmpmax  27714  stoweidlem14  27774  stoweidlem16  27776  stoweidlem24  27784  stoweidlem39  27799  stoweidlem50  27810  stoweidlem54  27814  stoweidlem57  27817  wallispilem3  27827  ndmafv  28014  usgra0v  28128  usgra1v  28137  uvtxisvtx  28173  2uasbanh  28383  bnj563  28845  bnj658  28853  bnj667  28854  bnj570  29010  bnj938  29042  bnj1001  29063  bnj1006  29064  bnj1049  29077  bnj1121  29088  bnj1173  29105  bnj1177  29109  bnj1245  29117  bnj1311  29127  bnj1321  29130  bnj1388  29136  bnj1398  29137  bnj1415  29141  bnj1417  29144  bnj1421  29145  bnj1442  29152  bnj1452  29155  bnj1489  29159  bnj1312  29161  ollat  29476  omlol  29503  cvlatl  29588  hlomcmcv  29619  2dim  29732  1dimN  29733  lcfl8b  31767  lclkrlem2  31795  lclkrslem1  31800  lclkrslem2  31801  lcfrlem9  31813  mapdval2N  31893  mapdordlem2  31900  mapdrvallem2  31908
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator