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  2767  eqimss  3243  pssss  3284  eldifi  3311  inss1  3402  ssunsn2  3789  pwssun  4315  sopo  4347  wefr  4399  ordtr  4422  opelxp1  4738  relop  4850  funmo  5287  funrel  5288  fnfun  5357  ffn  5405  f1f  5453  f1of1  5487  f1ofo  5495  isof1o  5838  eqopi  6172  1st2nd2  6175  reldmtpos  6258  swoer  6704  erdisj  6723  ecopover  6778  sdomdom  6905  inf3lemd  7344  mapfien  7415  cardprclem  7628  infxpenlem  7657  cardinfima  7740  dfac5lem4  7769  domtriomlem  8084  smobeth  8224  fpwwe2lem6  8273  fpwwe2lem7  8274  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  axrnegex  8800  axpre-sup  8807  eqlei  8958  zre  10044  nnssz  10059  supminf  10321  ixxss1  10690  ixxss2  10691  ixxss12  10692  lbioo  10703  ubioo  10704  iccss2  10736  elfzuz  10810  uzdisj  10872  splfv1  11486  sqrlem6  11749  rlimf  11991  lo1f  12008  lo1dm  12009  o1f  12019  o1dm  12020  fsumge0  12269  incexc2  12313  mertenslem2  12357  divalglem9  12616  bitsinv2  12650  bitsf1ocnv  12651  gcdcllem1  12706  prmnn  12777  prmind2  12785  nprm  12788  prmuz2  12792  isprm6  12804  exprmfct  12805  isprm5  12807  maxprmfct  12808  phibndlem  12854  phibnd  12855  dfphi2  12858  phimullem  12863  pclem  12907  pcprendvds2  12910  pcpre1  12911  expnprm  12966  prmreclem1  12979  1arith  12990  4sqlem15  13022  4sqlem16  13023  vdwlem5  13048  vdwlem6  13049  vdwlem8  13051  vdwlem9  13052  vdwlem11  13054  ramtlecl  13063  0ramcl  13086  firest  13353  acsmre  13570  posprs  14099  latpos  14171  dlatl  14314  pslem  14331  tsrlemax  14345  tsrps  14346  laps  14361  mndlem1  14387  grpmnd  14510  nsgsubg  14665  ghmgrp1  14701  ghmgrp2  14702  gimghm  14744  gagrp  14762  gaset  14763  efgredeu  15077  ablgrp  15110  cmnmnd  15120  cyggenod2  15188  cyggrp  15192  ablfac2  15340  crngrng  15367  dvdsrcl  15447  unitcl  15457  drngrng  15535  subrgrng  15564  subrgrcl  15566  srngrhm  15632  lmimlmhm  15833  lveclmod  15875  2idlcpbl  16002  divs1  16003  divsrhm  16005  lpirrng  16020  nzrrng  16029  domnnzr  16052  fldidom  16062  assalmod  16076  assarng  16077  assasca  16078  cygznlem1  16536  cygznlem3  16539  topontop  16680  tpstop  16693  clsval2  16803  mretopd  16845  perftop  16903  restfpw  16926  cntop1  16986  cntop2  16987  cnptop1  16988  cnptop2  16989  cnprcl  16991  t1ficld  17071  t0top  17073  t1top  17074  haustop  17075  regtop  17077  nrmtop  17080  cnrmtop  17081  pnrmnrm  17084  cmptop  17138  discmp  17141  tgcmp  17144  uncmp  17146  conndisj  17158  contop  17159  1stctop  17185  llytop  17214  nllytop  17215  txdis1cn  17345  hmeocn  17467  filfbas  17559  ufilfil  17615  flimtop  17676  flimfil  17680  alexsublem  17754  ptcmplem3  17764  tsmsfbas  17826  tsmslem1  17827  tsmsgsum  17837  tsmssubm  17841  tsmsres  17842  tsmsf1o  17843  tsmsmhm  17844  tsmsadd  17845  tsmsxplem1  17851  tsmsxplem2  17852  tsmsxp  17853  tlmtmd  17885  tlmlmod  17887  tlmtrg  17888  tvctlm  17895  isxmet2d  17908  metxmet  17915  xmstps  18015  msxms  18016  xmsxmet  18018  msmet  18019  stdbdxmet  18077  nrgngp  18189  nlmngp  18204  nlmlmod  18205  nlmnrg  18206  nvcnlm  18222  nmoi  18253  nghmrcl1  18257  nghmrcl2  18258  nmhmrcl1  18272  nmhmrcl2  18273  qdensere  18295  xrge0gsumle  18354  xrge0tsms  18355  metds0  18370  metdstri  18371  metdsre  18373  metdseq0  18374  metdscnlem  18375  metnrmlem1a  18378  metnrmlem1  18379  icopnfcnv  18456  icopnfhmeo  18457  cmetmet  18728  cmsms  18786  hlbn  18796  ovolicc1  18891  ovolicc2lem5  18896  mblss  18906  mbff  18998  mbfres  19015  mbfadd  19032  mbfsub  19033  i1fmbf  19046  mbfmul  19097  bddmulibl  19209  limcmpt  19249  dvcnvlem  19339  c1liplem1  19359  c1lip2  19361  fta1glem1  19567  fta1glem2  19568  fta1g  19569  fta1b  19571  ply1pid  19581  aacn  19713  ulmf2  19779  logdmnrp  20004  logdmss  20005  logcnlem2  20006  logcnlem3  20007  logcnlem4  20008  logcnlem5  20009  logcn  20010  dvloglem  20011  logf1o2  20013  efopnlem1  20019  logtayl2  20025  cxpcn  20101  cxpcn3lem  20103  cxpcn3  20104  resqrcn  20105  atandmneg  20218  atandmcj  20221  cosatan  20233  cosatanne0  20234  birthdaylem1  20262  areacl  20273  cxp2lim  20287  jensenlem2  20298  jensen  20299  wilth  20325  sqff1o  20436  dvdsdivcl  20437  fsumdvdsdiaglem  20439  dvdsflf1o  20443  muinv  20449  dvdsmulf1o  20450  mersenne  20482  bposlem3  20541  lgsqrlem1  20596  lgsqrlem2  20597  lgsqrlem3  20598  lgsqrlem4  20599  lgseisenlem3  20606  lgsquad2lem2  20614  2sqlem6  20624  chebbnd1  20637  chtppilim  20640  chpchtlim  20644  chpo1ub  20645  rplogsumlem1  20649  rplogsumlem2  20650  dchrmusumlema  20658  dchrvmasumiflem1  20666  dchrisum0flblem2  20674  dchrisum0lema  20679  dchrisum0lem2  20683  logsqvma  20707  selberg3lem2  20723  pntrsumo1  20730  selbergsb  20740  pnt2  20778  ostthlem2  20793  ostth2lem2  20799  ablogrpo  20967  smgrpismgm  21015  mndoissmgrp  21022  nmogtmnf  21364  bnnv  21461  hlobn  21483  hcauseq  21780  hlimseqi  21784  hlimveci  21785  shss  21805  sh0  21811  chsh  21820  lnopf  22455  bdopln  22457  nmopgtmnf  22464  hmopf  22470  lnfnf  22480  unopf1o  22512  elunop2  22609  elpjhmop  22781  stcltrlem1  22872  mdslle1i  22913  mdslle2i  22914  ballotlemfc0  23067  ballotlemfcc  23068  ballotlem5  23074  ballotlemscr  23093  ballotlemfg  23100  ballotlemfrc  23101  ballotlemfrceq  23103  ballotlemrinv0  23107  rabexgfGS  23187  ssnnssfz  23292  lmxrge0  23390  xrge0tsmsd  23397  esumpcvgval  23461  insiga  23513  brsiga  23529  measssd  23558  measinb2  23565  pwcntmeas  23569  mbfmbfm  23578  imambfm  23582  elmbfmvol2  23587  mbfmcnt  23588  domprobmeas  23628  cndprob01  23653  isrrvv  23661  dstrvprob  23687  subfacval3  23735  pcontop  23771  sconpcon  23773  cvmcn  23808  cvmliftlem10  23840  eupagra  23897  fundmpss  24193  predel  24254  sltres  24389  funpartfun  24553  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  axcontlem10  24673  outsideofcol  24828  itg2gt0cn  25006  fordisxex  25057  alneal1  25103  dfdir2  25394  dirpre  25396  isibg1a  26214  fnebas  26376  filnetlem3  26432  istotbnd3  26598  totbndmet  26599  sstotbnd2  26601  sstotbnd  26602  equivtotbnd  26605  bndmet  26608  totbndbnd  26616  prdstotbnd  26621  crngorngo  26728  prrngorngo  26779  divrngpr  26781  an3  26817  nacsacs  26887  eldiophelnn0  26946  jm2.17a  27150  jm2.17b  27151  jm2.17c  27152  jm2.27c  27203  jm3.1lem1  27213  jm3.1lem2  27214  jm3.1lem3  27215  lnmlmod  27280  lbslinds  27406  lnrrng  27419  mncply  27445  psgneu  27532  idomrootle  27614  idomodle  27615  hashgcdlem  27619  fnvinran  27788  cncmpmax  27806  stoweidlem14  27866  stoweidlem16  27868  stoweidlem24  27876  stoweidlem39  27891  stoweidlem50  27902  stoweidlem54  27906  stoweidlem57  27909  wallispilem3  27919  ndmafv  28108  usgra0v  28251  usgra1v  28260  uvtxisvtx  28303  2uasbanh  28626  bnj563  29088  bnj658  29096  bnj667  29097  bnj570  29253  bnj938  29285  bnj1001  29306  bnj1006  29307  bnj1049  29320  bnj1121  29331  bnj1173  29348  bnj1177  29352  bnj1245  29360  bnj1311  29370  bnj1321  29373  bnj1388  29379  bnj1398  29380  bnj1415  29384  bnj1417  29387  bnj1421  29388  bnj1442  29395  bnj1452  29398  bnj1489  29402  bnj1312  29404  ollat  30025  omlol  30052  cvlatl  30137  hlomcmcv  30168  2dim  30281  1dimN  30282  lcfl8b  32316  lclkrlem2  32344  lclkrslem1  32349  lclkrslem2  32350  lcfrlem9  32362  mapdval2N  32442  mapdordlem2  32449  mapdrvallem2  32457
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