Theorem simp1 1028

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

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  simpl1  1031  simpr1  1034  simp1i  1037  simp1d  1040  simp11  1058  simp21  1061  simp31  1064  syld3an3  1323  3ianorr  1350  intn3an1d  1397  stoic4a  1481  stoic4b  1482  rsp2e  2601  ifnetruedc  3681  issod  4459  elirr  4683  sotri2  5180  sotri3  5181  funtpg  5427  funimaexglem  5459  feq123  5520  ftpg  5890  fsnunf  5906  foco2  5949  fcofo  5980  f1oiso2  6023  riotass  6058  ovmpox  6207  ovmpoga  6208  caovimo  6273  ofeq  6295  ofrval  6303  fvn0elsuppb  6482  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  frecsuclem  6667  frecrdg  6669  domssr  7054  mapxpen  7138  diffifi  7188  unsnfidcex  7217  unsnfidcel  7218  unfidisj  7219  undifdc  7221  ssfidc  7235  iunfidisj  7250  fissfi  7253  sbthlemi9  7272  elfir  7297  fdcf1  7306  djuassen  7563  dftap2  7607  mulcanenq  7742  ltanqg  7757  addnnnq0  7806  distrlem4prl  7941  distrlem4pru  7942  distrprg  7945  aptipr  7998  addsrpr  8102  mulsrpr  8103  mulasssrg  8115  ltpsrprg  8160  axmulass  8230  axpre-ltadd  8243  mul31  8447  addsubass  8526  subcan2  8541  subsub2  8544  subsub4  8549  npncan3  8554  pnpcan  8555  pnncan  8557  subcan  8571  subdi  8702  ltadd1  8747  leadd1  8748  leadd2  8749  ltsubadd  8750  lesubadd  8752  ltaddsub  8754  leaddsub  8756  lesub1  8774  lesub2  8775  ltsub1  8776  ltsub2  8777  ltaddsublt  8889  gt0add  8891  apreap  8905  lemul1  8911  reapmul1lem  8912  reapmul1  8913  reapadd1  8914  remulext1  8917  remulext2  8918  apadd2  8927  mulext2  8931  mulap0r  8933  leltap  8943  ltap  8951  apsub1  8960  recexaplem2  8970  mulcanap  8983  mulcanap2  8984  divvalap  8994  divcanap2  9000  diveqap0  9002  divrecap  9008  divrecap2  9009  divdirap  9017  divcanap3  9018  div11ap  9020  muldivdirap  9027  divcanap5  9034  redivclap  9051  div2negap  9055  apmul1  9108  apmul2  9109  div2subap  9157  ltdiv1  9188  ltmuldiv  9194  lemuldiv  9201  lt2msq1  9205  ltdiv23  9212  lediv23  9213  squeeze0  9224  ofnegsub  9282  difgtsumgt  9693  zfidc  9702  gtndiv  9720  eluz2  9906  eluzsub  9931  peano2uz  9962  nn01to3  9996  divge1  10103  ledivge1le  10106  addlelt  10148  xaddass  10250  xleadd1  10256  xltadd1  10257  ixxssixx  10283  lbico1  10311  lbicc2  10365  icoshftf1o  10372  fzen  10426  fzrev3  10472  fzrevral2  10491  nelfzo  10537  elfzo0  10571  elfzo0z  10574  fzosplitprm1  10631  qbtwnre  10669  flqwordi  10701  flqword2  10702  adddivflid  10705  flltdivnn0lt  10717  modqcl  10741  mulqmod0  10745  modqmulnn  10757  modqabs2  10773  addmodid  10787  modifeq2int  10801  modqeqmodmin  10809  seqeq2  10866  seqeq3  10867  seq1g  10878  seqp1g  10881  exp3val  10956  expnegap0  10962  expgt1  10992  exprecap  10995  leexp2a  11007  expubnd  11011  sqdivap  11018  expnbnd  11079  mulsubdivbinom2ap  11127  bccmpl  11170  fihashss  11235  leisorel  11267  ccatass  11354  ccats1val2  11386  swrdval  11398  swrdval2  11401  swrdlen2  11412  swrdfv2  11413  pfxfv  11434  pfxn0  11438  pfxnd  11439  swrdswrd  11455  pfxswrd  11456  pfxpfx  11458  ccats1pfxeqbi  11492  s3cl  11536  s3fv0g  11541  s3fv1g  11542  s3fv2g  11543  shftfibg  11563  mulreap  11607  abssubne0  11835  maxleast  11957  lemininf  11978  ltmininf  11979  xrmaxltsup  12002  xrmaxaddlem  12004  xrmaxadd  12005  xrmineqinf  12013  xrltmininf  12014  xrminltinf  12016  xrminadd  12019  climuni  12037  reccn2ap  12057  isumz  12134  fsumsplitsnun  12164  geoisum1c  12265  prod1dc  12331  efltim  12443  dvdscmulr  12565  dvdsmulcr  12566  summodnegmod  12567  modmulconst  12568  dvdsmultr2  12578  dvdsexp  12606  mulmoddvds  12608  modremain  12674  divgcdz  12726  gcdaddm  12739  dvdsgcdb  12768  gcdass  12770  mulgcd  12771  gcddiv  12774  rplpwr  12782  uzwodc  12792  lcmdvdsb  12840  lcmass  12841  mulgcddvds  12850  qredeq  12852  qredeu  12853  rpmul  12854  divgcdcoprmex  12858  cncongr1  12859  rpexp  12909  rpexp12i  12911  odzcllem  12999  odzdvds  13002  odzphi  13003  pythagtriplem15  13035  pcpremul  13050  pcdiv  13059  pcqmul  13060  pcqdiv  13064  dvdsprmpweq  13092  sumhashdc  13104  pcfaclem  13106  qexpz  13109  ballotfilemfrcn0  13251  ctinf  13299  setsvala  13361  ressressg  13406  ressabsg  13407  rngbaseg  13467  ptex  13595  issubmnd  13732  ress0g  13733  imasmnd2  13736  grpasscan2  13846  grpidrcan  13847  grpidlcan  13848  grpinvadd  13860  grpsubeq0  13868  grppncan  13873  dfgrp3m  13881  grpsubpropd2  13887  imasgrp2  13890  mhmmnd  13896  mulgnegneg  13921  mulgaddcomlem  13925  mulgaddcom  13926  mulginvcom  13927  mulgmodid  13941  issubg  13953  nsgconj  13986  nsgid  13995  quselbasg  14010  quseccl0g  14011  ghmnsgima  14048  cmn4  14085  ablinvadd  14091  ablsub4  14094  abladdsub4  14095  ablpncan2  14097  gsumsncmn  14133  gsumconstcmn  14143  pwsinvg  14192  rngpropd  14229  imasrng  14230  issrg  14243  ringidss  14307  ringcom  14309  imasring  14342  unitmulcl  14393  unitmulclb  14394  dvrcl  14415  unitdvcl  14416  dvrcan1  14420  dvrcan3  14421  issubrng  14480  subrngpropd  14497  rrgeq0  14546  islmod  14600  lmodcom  14642  rmodislmodlem  14659  rmodislmod  14660  lss0cl  14678  lssvnegcl  14685  lssintclm  14693  lssincl  14694  lspss  14708  lspun  14711  lspsnvsi  14727  lsslsp  14738  rnglidlmmgm  14805  rnglidlmsgrp  14806  rnglidlrng  14807  qus2idrng  14834  qusmulrng  14841  psrbaglecl  14983  psrbagcon  14985  2basgeng  15106  clsss  15142  ntrss  15143  ntrin  15148  neiss  15174  restco  15198  restabs  15199  lmconst  15240  psmetsym  15353  psmetge0  15355  xmetge0  15389  xmetsym  15392  xmetresbl  15464  mopni3  15508  bdxmet  15525  bdmopn  15528  txmetcnp  15542  dvfvalap  15705  dvid  15719  dvidre  15721  dvcnp2cntop  15723  elplyr  15764  ply1term  15767  ptolemy  15848  logfac  15918  rpcxpadd  15930  rpmulcxp  15934  rpdivcxp  15936  cxpmul  15937  rpcxple2  15943  rpcxplt2  15944  cxpcom  15963  rplogbval  15970  rplogbcl  15971  rprelogbmulexp  15981  relogbexpap  15983  logbleb  15986  logblt  15987  rplogbcxp  15988  rpcxplogb  15989  sgmppw  16020  lgslem1  16033  lgsfcl2  16039  lgsneg  16057  lgsne0  16071  lgssq2  16074  lgsdirnn0  16080  gausslemma2dlem1a  16091  lgsquad  16113  2lgsoddprmlem2  16139  funvtxvalg  16191  funiedgvalg  16192  lpvtx  16234  upgrex  16258  subumgredg2en  16426  iedginwlk  16512  eulerpathprum  16635  dichmul0or  16674