Theorem simplbi 457

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

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 194	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simpld 456	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  3simpa  978  xoror  1350  sbequ2  1701  reurex  2927  eqimss  3396  pssss  3439  eldifi  3466  inss1  3558  ssunsn2  4020  pwssun  4614  sopo  4645  wefr  4697  ordtr  4720  opelxp1  4859  relop  4977  xpdifid  5254  funmo  5422  funrel  5423  fnfun  5496  ffn  5547  f1f  5594  f1of1  5628  f1ofo  5636  isof1o  6003  eqopi  6599  1st2nd2  6602  reldmtpos  6742  swoer  7117  erdisj  7136  ecopover  7192  sdomdom  7325  mapfien  7645  inf3lemd  7821  mapfienOLD  7915  cardprclem  8137  infxpenlem  8168  cardinfima  8255  dfac5lem4  8284  domtriomlem  8599  smobeth  8738  fpwwe2lem6  8789  fpwwe2lem7  8790  fpwwe2lem12  8795  fpwwe2lem13  8796  fpwwe2  8797  axrnegex  9316  axpre-sup  9323  zre  10637  nnssz  10653  ixxss1  11305  ixxss2  11306  ixxss12  11307  lbioo  11318  ubioo  11319  iccss2  11353  elfzuz  11435  uzdisj  11514  0wrd0  12236  splfv1  12380  sqrlem6  12720  rlimf  12962  lo1f  12979  lo1dm  12980  o1f  12990  o1dm  12991  fsumge0  13240  mertenslem2  13327  divalglem9  13587  bitsinv2  13621  bitsf1ocnv  13622  gcdcllem1  13677  prmnn  13748  prmind2  13756  nprm  13759  prmuz2  13763  isprm6  13777  exprmfct  13778  isprm5  13780  maxprmfct  13781  phibndlem  13827  phibnd  13828  dfphi2  13831  phimullem  13836  pclem  13887  pcprendvds2  13890  pcpre1  13891  expnprm  13946  prmreclem1  13959  1arith  13970  4sqlem15  14002  4sqlem16  14003  vdwlem5  14028  vdwlem6  14029  vdwlem8  14031  vdwlem9  14032  vdwlem11  14034  ramtlecl  14043  0ramcl  14066  firest  14353  acsmre  14572  posprs  15101  latpos  15202  clatpos  15262  dlatl  15347  pslem  15358  tsrlemax  15372  tsrps  15373  mndlem1  15401  grpmnd  15529  nsgsubg  15692  ghmgrp1  15728  ghmgrp2  15729  gimghm  15771  gagrp  15789  gaset  15790  psgneu  15991  efgredeu  16228  ablgrp  16261  cmnmnd  16271  cyggenod2  16341  cyggrp  16345  ablfac2  16563  crngrng  16590  dvdsrcl  16674  unitcl  16684  drngrng  16762  subrgrng  16791  subrgrcl  16793  srngrhm  16859  lmimlmhm  17066  lveclmod  17108  2idlcpbl  17237  divs1  17238  divsrhm  17240  lpirrng  17255  nzrrng  17264  domnnzr  17288  fldidom  17298  assalmod  17312  assarng  17313  assasca  17314  cygznlem1  17840  cygznlem3  17843  lbslinds  18103  gsummatr01lem1  18302  topontop  18372  tpstop  18385  clsval2  18495  mretopd  18537  neiptoptop  18576  perftop  18601  restfpw  18624  cntop1  18685  cntop2  18686  cnptop1  18687  cnptop2  18688  cnprcl  18690  t1ficld  18772  t0top  18774  t1top  18775  haustop  18776  regtop  18778  nrmtop  18781  cnrmtop  18782  pnrmnrm  18785  cmptop  18839  discmp  18842  tgcmp  18845  uncmp  18847  conndisj  18861  contop  18862  1stctop  18888  llytop  18917  nllytop  18918  hmeocn  19174  filfbas  19262  ufilfil  19318  flimtop  19379  flimfil  19383  alexsublem  19457  ptcmplem3  19467  tsmsfbas  19539  tsmslem1  19540  tsmsgsum  19550  tsmsgsumOLD  19553  tsmssubm  19557  tsmsresOLD  19558  tsmsres  19559  tsmsf1o  19560  tsmsmhm  19561  tsmsadd  19562  tsmsxplem1  19568  tsmsxplem2  19569  tsmsxp  19570  tlmtmd  19602  tlmlmod  19604  tlmtrg  19605  tvctlm  19612  ressust  19680  uspreg  19690  ucncn  19701  neipcfilu  19712  cuspusp  19716  isxmet2d  19743  metxmet  19750  xmstps  19869  msxms  19870  xmsxmet  19872  msmet  19873  stdbdxmet  19931  nrgngp  20084  nlmngp  20099  nlmlmod  20100  nlmnrg  20101  nvcnlm  20117  nmoi  20148  nghmrcl1  20152  nghmrcl2  20153  nmhmrcl1  20167  nmhmrcl2  20168  qdensere  20190  xrge0gsumle  20251  xrge0tsms  20252  metds0  20267  metdstri  20268  metdsre  20270  metdseq0  20271  metdscnlem  20272  metnrmlem1a  20275  metnrmlem1  20276  icopnfcnv  20355  icopnfhmeo  20356  cvsclm  20520  cmetmet  20638  cmsms  20700  hlbn  20716  ovolicc1  20840  ovolicc2lem5  20845  mblss  20855  mbff  20946  mbfres  20963  mbfadd  20980  mbfsub  20981  i1fmbf  20994  mbfmul  21045  bddmulibl  21157  limcmpt  21199  c1liplem1  21309  c1lip2  21311  fta1glem1  21521  fta1glem2  21522  fta1g  21523  fta1b  21525  ply1pid  21535  aacn  21667  ulmf2  21733  logdmnrp  21970  logdmss  21971  logcnlem2  21972  logcnlem3  21973  logcnlem4  21974  logcnlem5  21975  logcn  21976  dvloglem  21977  logf1o2  21979  efopnlem1  21985  logtayl2  21991  cxpcn  22067  cxpcn3lem  22069  cxpcn3  22070  resqrcn  22071  atandmneg  22185  atandmcj  22188  cosatan  22200  cosatanne0  22201  birthdaylem1  22229  areacl  22240  cxp2lim  22254  jensenlem2  22265  jensen  22266  wilth  22293  sqff1o  22404  dvdsmulf1o  22418  mersenne  22450  bposlem3  22509  lgsqrlem1  22564  lgsqrlem2  22565  lgsqrlem3  22566  lgsqrlem4  22567  lgseisenlem3  22574  lgsquad2lem2  22582  2sqlem6  22592  chebbnd1  22605  chtppilim  22608  chpchtlim  22612  chpo1ub  22613  rplogsumlem1  22617  rplogsumlem2  22618  dchrmusumlema  22626  dchrvmasumiflem1  22634  dchrisum0flblem2  22642  dchrisum0lema  22647  dchrisum0lem2  22651  selberg3lem2  22691  pntrsumo1  22698  selbergsb  22708  pnt2  22746  ostthlem2  22761  ostth2lem2  22767  tglineeltr  22907  axcontlem2  23033  axcontlem7  23038  axcontlem8  23039  axcontlem10  23041  uhgra0v  23066  usgra0v  23112  usgra1v  23130  eupagra  23409  ablogrpo  23593  smgrpismgm  23641  mndoissmgrp  23648  nmogtmnf  23992  bnnv  24089  hlobn  24111  hcauseq  24409  hlimseqi  24413  hlimveci  24414  shss  24434  sh0  24440  chsh  24449  lnopf  25085  bdopln  25087  nmopgtmnf  25094  hmopf  25100  lnfnf  25110  unopf1o  25142  elunop2  25239  elpjhmop  25411  stcltrlem1  25502  mdslle1i  25543  mdslle2i  25544  rabexgfGS  25709  suppss3  25850  ssnnssfz  25898  tospos  25941  ogrpgrp  25989  ogrpinvOLD  26001  ogrpinv0le  26002  ogrpsub  26003  ogrpaddlt  26004  archirng  26028  archirngz  26029  archiabllem1a  26031  archiabllem1b  26032  archiabllem1  26033  archiabllem2a  26034  archiabllem2c  26035  archiabllem2b  26036  archiabllem2  26037  xrge0tsmsd  26105  ofldfld  26130  ofldlt1  26133  ofldchr  26134  isarchiofld  26137  reofld  26161  rearchi  26163  lmxrge0  26235  qqhrhm  26271  esumpcvgval  26380  measssd  26482  elmbfmvol2  26535  sibfinima  26572  eulerpartlemr  26604  eulerpartlemgf  26609  fiblem  26628  domprobmeas  26640  ballotlemscr  26748  ballotlemfg  26755  ballotlemfrc  26756  ballotlemfrceq  26758  ballotlemrinv0  26762  signstfveq0  26825  subfacval3  26924  pcontop  26961  sconpcon  26963  cvmcn  26998  cvmliftlem10  27030  fundmpss  27423  predel  27490  sltres  27651  funpartfun  27820  outsideofcol  28010  itg2addnc  28287  itg2gt0cn  28288  ftc1anclem3  28310  fnebas  28386  filnetlem3  28442  istotbnd3  28511  totbndmet  28512  sstotbnd2  28514  sstotbnd  28515  equivtotbnd  28518  bndmet  28521  totbndbnd  28529  prdstotbnd  28534  crngorngo  28641  prrngorngo  28692  divrngpr  28694  an3  28837  nacsacs  28887  eldiophelnn0  28944  jm2.17a  29145  jm2.17b  29146  jm2.17c  29147  jm2.27c  29198  jm3.1lem1  29208  jm3.1lem2  29209  jm3.1lem3  29210  lnmlmod  29274  lnrrng  29310  mncply  29336  idomrootle  29402  idomodle  29403  hashgcdlem  29407  areaquad  29434  stoweidlem14  29652  stoweidlem16  29654  stoweidlem24  29662  stoweidlem39  29677  stoweidlem50  29688  stoweidlem51  29689  stoweidlem54  29692  stoweidlem57  29695  wallispilem3  29705  ndmafv  29889  rusgranumwlks  30417  frgrawopreg  30485  2uasbanh  30968  bnj563  31434  bnj658  31442  bnj667  31443  bnj570  31597  bnj938  31629  bnj1001  31650  bnj1006  31651  bnj1049  31664  bnj1121  31675  bnj1173  31692  bnj1177  31696  bnj1245  31704  bnj1311  31714  bnj1321  31717  bnj1388  31723  bnj1398  31724  bnj1415  31728  bnj1417  31731  bnj1421  31732  bnj1442  31739  bnj1452  31742  bnj1489  31746  bnj1312  31748  ollat  32428  omlol  32455  cvlatl  32540  hlomcmcv  32571  2dim  32684  1dimN  32685  lcfl8b  34719  lclkrlem2  34747  lclkrslem1  34752  lclkrslem2  34753  lcfrlem9  34765  mapdval2N  34845  mapdordlem2  34852  mapdrvallem2  34860