Theorem simp1 999

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simpl1  1002  simpr1  1005  simp1i  1008  simp1d  1011  simp11  1029  simp21  1032  simp31  1035  syld3an3  1294  3ianorr  1320  stoic4a  1443  stoic4b  1444  rsp2e  2548  ifnetruedc  3603  issod  4355  elirr  4578  sotri2  5068  sotri3  5069  funtpg  5310  funimaexglem  5342  feq123  5402  ftpg  5749  fsnunf  5765  foco2  5803  fcofo  5834  f1oiso2  5877  riotass  5908  ovmpox  6055  ovmpoga  6056  caovimo  6121  ofeq  6142  ofrval  6150  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  frecsuclem  6473  frecrdg  6475  mapxpen  6918  diffifi  6964  unsnfidcex  6990  unsnfidcel  6991  unfidisj  6992  undifdc  6994  ssfidc  7007  iunfidisj  7021  sbthlemi9  7040  elfir  7048  djuassen  7302  dftap2  7336  mulcanenq  7471  ltanqg  7486  addnnnq0  7535  distrlem4prl  7670  distrlem4pru  7671  distrprg  7674  aptipr  7727  addsrpr  7831  mulsrpr  7832  mulasssrg  7844  ltpsrprg  7889  axmulass  7959  axpre-ltadd  7972  mul31  8176  addsubass  8255  subcan2  8270  subsub2  8273  subsub4  8278  npncan3  8283  pnpcan  8284  pnncan  8286  subcan  8300  subdi  8430  ltadd1  8475  leadd1  8476  leadd2  8477  ltsubadd  8478  lesubadd  8480  ltaddsub  8482  leaddsub  8484  lesub1  8502  lesub2  8503  ltsub1  8504  ltsub2  8505  ltaddsublt  8617  gt0add  8619  apreap  8633  lemul1  8639  reapmul1lem  8640  reapmul1  8641  reapadd1  8642  remulext1  8645  remulext2  8646  apadd2  8655  mulext2  8659  mulap0r  8661  leltap  8671  ltap  8679  apsub1  8688  recexaplem2  8698  mulcanap  8711  mulcanap2  8712  divvalap  8720  divcanap2  8726  diveqap0  8728  divrecap  8734  divrecap2  8735  divdirap  8743  divcanap3  8744  div11ap  8746  muldivdirap  8753  divcanap5  8760  redivclap  8777  div2negap  8781  apmul1  8834  apmul2  8835  div2subap  8883  ltdiv1  8914  ltmuldiv  8920  lemuldiv  8927  lt2msq1  8931  ltdiv23  8938  lediv23  8939  squeeze0  8950  ofnegsub  9008  difgtsumgt  9414  gtndiv  9440  eluz2  9626  eluzsub  9650  peano2uz  9676  nn01to3  9710  divge1  9817  ledivge1le  9820  addlelt  9862  xaddass  9963  xleadd1  9969  xltadd1  9970  ixxssixx  9996  lbico1  10024  lbicc2  10078  icoshftf1o  10085  fzen  10137  fzrev3  10181  fzrevral2  10200  nelfzo  10246  elfzo0  10277  elfzo0z  10279  fzosplitprm1  10329  qbtwnre  10365  flqwordi  10397  flqword2  10398  adddivflid  10401  flltdivnn0lt  10413  modqcl  10437  mulqmod0  10441  modqmulnn  10453  modqabs2  10469  addmodid  10483  modifeq2int  10497  modqeqmodmin  10505  seqeq2  10562  seqeq3  10563  seq1g  10574  seqp1g  10577  exp3val  10652  expnegap0  10658  expgt1  10688  exprecap  10691  leexp2a  10703  expubnd  10707  sqdivap  10714  expnbnd  10774  mulsubdivbinom2ap  10822  bccmpl  10865  fihashss  10927  leisorel  10948  shftfibg  11004  mulreap  11048  abssubne0  11275  maxleast  11397  lemininf  11418  ltmininf  11419  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  xrmineqinf  11453  xrltmininf  11454  xrminltinf  11456  xrminadd  11459  climuni  11477  reccn2ap  11497  isumz  11573  fsumsplitsnun  11603  geoisum1c  11704  prod1dc  11770  efltim  11882  dvdscmulr  12004  dvdsmulcr  12005  summodnegmod  12006  modmulconst  12007  dvdsmultr2  12017  dvdsexp  12045  mulmoddvds  12047  modremain  12113  divgcdz  12165  gcdaddm  12178  dvdsgcdb  12207  gcdass  12209  mulgcd  12210  gcddiv  12213  rplpwr  12221  uzwodc  12231  lcmdvdsb  12279  lcmass  12280  mulgcddvds  12289  qredeq  12291  qredeu  12292  rpmul  12293  divgcdcoprmex  12297  cncongr1  12298  rpexp  12348  rpexp12i  12350  odzcllem  12438  odzdvds  12441  odzphi  12442  pythagtriplem15  12474  pcpremul  12489  pcdiv  12498  pcqmul  12499  pcqdiv  12503  dvdsprmpweq  12531  sumhashdc  12543  pcfaclem  12545  qexpz  12548  ctinf  12674  setsvala  12736  ressressg  12780  ressabsg  12781  rngbaseg  12840  ptex  12968  issubmnd  13146  ress0g  13147  imasmnd2  13156  gsumfzz  13199  grpasscan2  13268  grpidrcan  13269  grpidlcan  13270  grpinvadd  13282  grpsubeq0  13290  grppncan  13295  dfgrp3m  13303  grpsubpropd2  13309  pwsinvg  13316  imasgrp2  13318  mhmmnd  13324  mulgnegneg  13349  mulgaddcomlem  13353  mulgaddcom  13354  mulginvcom  13355  mulgmodid  13369  issubg  13381  nsgconj  13414  nsgid  13423  quselbasg  13438  quseccl0g  13439  ghmnsgima  13476  cmn4  13513  ablinvadd  13518  ablsub4  13521  abladdsub4  13522  ablpncan2  13524  rngpropd  13589  imasrng  13590  issrg  13599  ringidss  13663  ringcom  13665  imasring  13698  unitmulcl  13747  unitmulclb  13748  dvrcl  13769  unitdvcl  13770  dvrcan1  13774  dvrcan3  13775  issubrng  13833  subrngpropd  13850  rrgeq0  13899  islmod  13925  lmodcom  13967  rmodislmodlem  13984  rmodislmod  13985  lss0cl  14003  lssvnegcl  14010  lssintclm  14018  lssincl  14019  lspss  14033  lspun  14036  lspsnvsi  14052  lsslsp  14063  rnglidlmmgm  14130  rnglidlmsgrp  14131  rnglidlrng  14132  qus2idrng  14159  qusmulrng  14166  2basgeng  14426  clsss  14462  ntrss  14463  ntrin  14468  neiss  14494  restco  14518  restabs  14519  lmconst  14560  psmetsym  14673  psmetge0  14675  xmetge0  14709  xmetsym  14712  xmetresbl  14784  mopni3  14828  bdxmet  14845  bdmopn  14848  txmetcnp  14862  dvfvalap  15025  dvid  15039  dvidre  15041  dvcnp2cntop  15043  elplyr  15084  ply1term  15087  ptolemy  15168  rpcxpadd  15249  rpmulcxp  15253  rpdivcxp  15255  cxpmul  15256  rpcxple2  15262  rpcxplt2  15263  cxpcom  15282  rplogbval  15289  rplogbcl  15290  rprelogbmulexp  15300  relogbexpap  15302  logbleb  15305  logblt  15306  rplogbcxp  15307  rpcxplogb  15308  sgmppw  15336  lgslem1  15349  lgsfcl2  15355  lgsneg  15373  lgsne0  15387  lgssq2  15390  lgsdirnn0  15396  gausslemma2dlem1a  15407  lgsquad  15429  2lgsoddprmlem2  15455