Theorem simp1 987

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp1	|- ( ( ph /\ ps /\ ch ) -> ph )

Proof of Theorem simp1

Step	Hyp	Ref	Expression
1		3simpa 984	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simpld 111	1 |- ( ( ph /\ ps /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpl1  990  simpr1  993  simp1i  996  simp1d  999  simp11  1017  simp21  1020  simp31  1023  syld3an3  1273  3ianorr  1299  stoic4a  1420  stoic4b  1421  rsp2e  2516  issod  4296  elirr  4517  sotri2  5000  sotri3  5001  funtpg  5238  funimaexglem  5270  feq123  5328  ftpg  5668  fsnunf  5684  foco2  5721  fcofo  5751  f1oiso2  5794  riotass  5824  ovmpox  5966  ovmpoga  5967  caovimo  6031  ofeq  6051  ofrval  6059  tfr1onlembxssdm  6307  tfrcllembxssdm  6320  frecsuclem  6370  frecrdg  6372  mapxpen  6810  diffifi  6856  unsnfidcex  6881  unsnfidcel  6882  unfidisj  6883  undifdc  6885  ssfidc  6896  iunfidisj  6907  sbthlemi9  6926  elfir  6934  djuassen  7169  mulcanenq  7322  ltanqg  7337  addnnnq0  7386  distrlem4prl  7521  distrlem4pru  7522  distrprg  7525  aptipr  7578  addsrpr  7682  mulsrpr  7683  mulasssrg  7695  ltpsrprg  7740  axmulass  7810  axpre-ltadd  7823  mul31  8025  addsubass  8104  subcan2  8119  subsub2  8122  subsub4  8127  npncan3  8132  pnpcan  8133  pnncan  8135  subcan  8149  subdi  8279  ltadd1  8323  leadd1  8324  leadd2  8325  ltsubadd  8326  lesubadd  8328  ltaddsub  8330  leaddsub  8332  lesub1  8350  lesub2  8351  ltsub1  8352  ltsub2  8353  ltaddsublt  8465  gt0add  8467  apreap  8481  lemul1  8487  reapmul1lem  8488  reapmul1  8489  reapadd1  8490  remulext1  8493  remulext2  8494  apadd2  8503  mulext2  8507  mulap0r  8509  leltap  8519  ltap  8527  apsub1  8536  recexaplem2  8545  mulcanap  8558  mulcanap2  8559  divvalap  8566  divcanap2  8572  diveqap0  8574  divrecap  8580  divrecap2  8581  divdirap  8589  divcanap3  8590  div11ap  8592  muldivdirap  8599  divcanap5  8606  redivclap  8623  div2negap  8627  apmul1  8680  apmul2  8681  div2subap  8729  ltdiv1  8759  ltmuldiv  8765  lemuldiv  8772  lt2msq1  8776  ltdiv23  8783  lediv23  8784  squeeze0  8795  difgtsumgt  9256  gtndiv  9282  eluz2  9468  eluzsub  9491  peano2uz  9517  nn01to3  9551  divge1  9655  ledivge1le  9658  addlelt  9700  xaddass  9801  xleadd1  9807  xltadd1  9808  ixxssixx  9834  lbico1  9862  lbicc2  9916  icoshftf1o  9923  fzen  9974  fzrev3  10018  fzrevral2  10037  elfzo0  10113  elfzo0z  10115  fzosplitprm1  10165  qbtwnre  10188  flqwordi  10219  flqword2  10220  adddivflid  10223  flltdivnn0lt  10235  modqcl  10257  mulqmod0  10261  modqmulnn  10273  modqabs2  10289  addmodid  10303  modifeq2int  10317  modqeqmodmin  10325  seqeq2  10380  seqeq3  10381  exp3val  10453  expnegap0  10459  expgt1  10489  exprecap  10492  leexp2a  10504  expubnd  10508  sqdivap  10515  expnbnd  10574  bccmpl  10663  fihashss  10725  leisorel  10746  shftfibg  10758  mulreap  10802  abssubne0  11029  maxleast  11151  lemininf  11171  ltmininf  11172  xrmaxltsup  11195  xrmaxaddlem  11197  xrmaxadd  11198  xrmineqinf  11206  xrltmininf  11207  xrminltinf  11209  xrminadd  11212  climuni  11230  reccn2ap  11250  isumz  11326  fsumsplitsnun  11356  geoisum1c  11457  prod1dc  11523  efltim  11635  dvdscmulr  11756  dvdsmulcr  11757  summodnegmod  11758  modmulconst  11759  dvdsmultr2  11769  dvdsexp  11795  mulmoddvds  11797  modremain  11862  divgcdz  11900  gcdaddm  11913  dvdsgcdb  11942  gcdass  11944  mulgcd  11945  gcddiv  11948  rplpwr  11956  uzwodc  11966  lcmdvdsb  12012  lcmass  12013  mulgcddvds  12022  qredeq  12024  qredeu  12025  rpmul  12026  divgcdcoprmex  12030  cncongr1  12031  rpexp  12081  rpexp12i  12083  odzcllem  12170  odzdvds  12173  odzphi  12174  pythagtriplem15  12206  pcpremul  12221  pcdiv  12230  pcqmul  12231  pcqdiv  12235  dvdsprmpweq  12262  sumhashdc  12273  pcfaclem  12275  qexpz  12278  ctinf  12359  setsvala  12421  ressid2  12449  ressval2  12450  rngbaseg  12506  2basgeng  12682  clsss  12718  ntrss  12719  ntrin  12724  neiss  12750  restco  12774  restabs  12775  lmconst  12816  psmetsym  12929  psmetge0  12931  xmetge0  12965  xmetsym  12968  xmetresbl  13040  mopni3  13084  bdxmet  13101  bdmopn  13104  txmetcnp  13118  dvfvalap  13250  dvid  13262  dvcnp2cntop  13263  ptolemy  13345  rpcxpadd  13426  rpmulcxp  13430  rpdivcxp  13432  cxpmul  13433  rpcxple2  13438  rpcxplt2  13439  cxpcom  13457  rplogbval  13463  rplogbcl  13464  rprelogbmulexp  13474  relogbexpap  13476  logbleb  13479  logblt  13480  rplogbcxp  13481  rpcxplogb  13482  lgslem1  13501  lgsfcl2  13507  lgsneg  13525  lgsne0  13539  lgssq2  13542  lgsdirnn0  13548