Theorem simp1 997

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 994	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simpld 112	1 |- ( ( ph /\ ps /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simpl1  1000  simpr1  1003  simp1i  1006  simp1d  1009  simp11  1027  simp21  1030  simp31  1033  syld3an3  1283  3ianorr  1309  stoic4a  1432  stoic4b  1433  rsp2e  2528  issod  4320  elirr  4541  sotri2  5027  sotri3  5028  funtpg  5268  funimaexglem  5300  feq123  5358  ftpg  5701  fsnunf  5717  foco2  5755  fcofo  5785  f1oiso2  5828  riotass  5858  ovmpox  6003  ovmpoga  6004  caovimo  6068  ofeq  6085  ofrval  6093  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  frecsuclem  6407  frecrdg  6409  mapxpen  6848  diffifi  6894  unsnfidcex  6919  unsnfidcel  6920  unfidisj  6921  undifdc  6923  ssfidc  6934  iunfidisj  6945  sbthlemi9  6964  elfir  6972  djuassen  7216  dftap2  7250  mulcanenq  7384  ltanqg  7399  addnnnq0  7448  distrlem4prl  7583  distrlem4pru  7584  distrprg  7587  aptipr  7640  addsrpr  7744  mulsrpr  7745  mulasssrg  7757  ltpsrprg  7802  axmulass  7872  axpre-ltadd  7885  mul31  8088  addsubass  8167  subcan2  8182  subsub2  8185  subsub4  8190  npncan3  8195  pnpcan  8196  pnncan  8198  subcan  8212  subdi  8342  ltadd1  8386  leadd1  8387  leadd2  8388  ltsubadd  8389  lesubadd  8391  ltaddsub  8393  leaddsub  8395  lesub1  8413  lesub2  8414  ltsub1  8415  ltsub2  8416  ltaddsublt  8528  gt0add  8530  apreap  8544  lemul1  8550  reapmul1lem  8551  reapmul1  8552  reapadd1  8553  remulext1  8556  remulext2  8557  apadd2  8566  mulext2  8570  mulap0r  8572  leltap  8582  ltap  8590  apsub1  8599  recexaplem2  8609  mulcanap  8622  mulcanap2  8623  divvalap  8631  divcanap2  8637  diveqap0  8639  divrecap  8645  divrecap2  8646  divdirap  8654  divcanap3  8655  div11ap  8657  muldivdirap  8664  divcanap5  8671  redivclap  8688  div2negap  8692  apmul1  8745  apmul2  8746  div2subap  8794  ltdiv1  8825  ltmuldiv  8831  lemuldiv  8838  lt2msq1  8842  ltdiv23  8849  lediv23  8850  squeeze0  8861  difgtsumgt  9322  gtndiv  9348  eluz2  9534  eluzsub  9557  peano2uz  9583  nn01to3  9617  divge1  9723  ledivge1le  9726  addlelt  9768  xaddass  9869  xleadd1  9875  xltadd1  9876  ixxssixx  9902  lbico1  9930  lbicc2  9984  icoshftf1o  9991  fzen  10043  fzrev3  10087  fzrevral2  10106  elfzo0  10182  elfzo0z  10184  fzosplitprm1  10234  qbtwnre  10257  flqwordi  10288  flqword2  10289  adddivflid  10292  flltdivnn0lt  10304  modqcl  10326  mulqmod0  10330  modqmulnn  10342  modqabs2  10358  addmodid  10372  modifeq2int  10386  modqeqmodmin  10394  seqeq2  10449  seqeq3  10450  exp3val  10522  expnegap0  10528  expgt1  10558  exprecap  10561  leexp2a  10573  expubnd  10577  sqdivap  10584  expnbnd  10644  mulsubdivbinom2ap  10691  bccmpl  10734  fihashss  10796  leisorel  10817  shftfibg  10829  mulreap  10873  abssubne0  11100  maxleast  11222  lemininf  11242  ltmininf  11243  xrmaxltsup  11266  xrmaxaddlem  11268  xrmaxadd  11269  xrmineqinf  11277  xrltmininf  11278  xrminltinf  11280  xrminadd  11283  climuni  11301  reccn2ap  11321  isumz  11397  fsumsplitsnun  11427  geoisum1c  11528  prod1dc  11594  efltim  11706  dvdscmulr  11827  dvdsmulcr  11828  summodnegmod  11829  modmulconst  11830  dvdsmultr2  11840  dvdsexp  11867  mulmoddvds  11869  modremain  11934  divgcdz  11972  gcdaddm  11985  dvdsgcdb  12014  gcdass  12016  mulgcd  12017  gcddiv  12020  rplpwr  12028  uzwodc  12038  lcmdvdsb  12084  lcmass  12085  mulgcddvds  12094  qredeq  12096  qredeu  12097  rpmul  12098  divgcdcoprmex  12102  cncongr1  12103  rpexp  12153  rpexp12i  12155  odzcllem  12242  odzdvds  12245  odzphi  12246  pythagtriplem15  12278  pcpremul  12293  pcdiv  12302  pcqmul  12303  pcqdiv  12307  dvdsprmpweq  12334  sumhashdc  12345  pcfaclem  12347  qexpz  12350  ctinf  12431  setsvala  12493  ressressg  12534  ressabsg  12535  rngbaseg  12594  ptex  12713  issubmnd  12843  ress0g  12844  grpasscan2  12934  grpidrcan  12935  grpidlcan  12936  grpinvadd  12948  grpsubeq0  12956  grppncan  12961  dfgrp3m  12969  grpsubpropd2  12975  mhmmnd  12980  mulgnegneg  13002  mulgaddcomlem  13006  mulgaddcom  13007  mulginvcom  13008  mulgmodid  13022  issubg  13033  nsgconj  13066  nsgid  13075  cmn4  13108  ablinvadd  13113  ablsub4  13116  abladdsub4  13117  ablpncan2  13119  issrg  13148  ringidss  13212  ringcom  13214  unitmulcl  13282  unitmulclb  13283  dvrcl  13304  unitdvcl  13305  dvrcan1  13309  dvrcan3  13310  islmod  13381  lmodcom  13423  rmodislmodlem  13440  rmodislmod  13441  2basgeng  13585  clsss  13621  ntrss  13622  ntrin  13627  neiss  13653  restco  13677  restabs  13678  lmconst  13719  psmetsym  13832  psmetge0  13834  xmetge0  13868  xmetsym  13871  xmetresbl  13943  mopni3  13987  bdxmet  14004  bdmopn  14007  txmetcnp  14021  dvfvalap  14153  dvid  14165  dvcnp2cntop  14166  ptolemy  14248  rpcxpadd  14329  rpmulcxp  14333  rpdivcxp  14335  cxpmul  14336  rpcxple2  14341  rpcxplt2  14342  cxpcom  14360  rplogbval  14366  rplogbcl  14367  rprelogbmulexp  14377  relogbexpap  14379  logbleb  14382  logblt  14383  rplogbcxp  14384  rpcxplogb  14385  lgslem1  14404  lgsfcl2  14410  lgsneg  14428  lgsne0  14442  lgssq2  14445  lgsdirnn0  14451  2lgsoddprmlem2  14457