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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used 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  3684  issod  4464  elirr  4688  sotri2  5185  sotri3  5186  funtpg  5432  funimaexglem  5464  feq123  5525  ftpg  5899  fsnunf  5915  foco2  5959  fcofo  5990  f1oiso2  6033  riotass  6068  ovmpox  6217  ovmpoga  6218  caovimo  6283  ofeq  6305  ofrval  6313  fvn0elsuppb  6492  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  diffifi  7198  unsnfidcex  7227  unsnfidcel  7228  unfidisj  7229  undifdc  7231  ssfidc  7245  iunfidisj  7260  fissfi  7263  sbthlemi9  7282  elfir  7307  fdcf1  7316  djuassen  7574  dftap2  7618  mulcanenq  7753  ltanqg  7768  addnnnq0  7817  distrlem4prl  7952  distrlem4pru  7953  distrprg  7956  aptipr  8009  addsrpr  8113  mulsrpr  8114  mulasssrg  8126  ltpsrprg  8171  axmulass  8241  axpre-ltadd  8254  mul31  8459  addsubass  8538  subcan2  8553  subsub2  8556  subsub4  8561  npncan3  8566  pnpcan  8567  pnncan  8569  subcan  8583  subdi  8714  ltadd1  8759  leadd1  8760  leadd2  8761  ltsubadd  8762  lesubadd  8764  ltaddsub  8766  leaddsub  8768  lesub1  8786  lesub2  8787  ltsub1  8788  ltsub2  8789  ltaddsublt  8902  gt0add  8904  apreap  8918  lemul1  8924  reapmul1lem  8925  reapmul1  8926  reapadd1  8927  remulext1  8930  remulext2  8931  apadd2  8940  mulext2  8944  mulap0r  8946  leltap  8956  ltap  8964  apsub1  8973  recexaplem2  8983  mulcanap  8996  mulcanap2  8997  divvalap  9007  divcanap2  9013  diveqap0  9015  divrecap  9021  divrecap2  9022  divdirap  9030  divcanap3  9031  div11ap  9033  muldivdirap  9040  divcanap5  9047  redivclap  9064  div2negap  9068  apmul1  9121  apmul2  9122  div2subap  9170  ltdiv1  9201  ltmuldiv  9207  lemuldiv  9214  lt2msq1  9218  ltdiv23  9225  lediv23  9226  squeeze0  9237  ofnegsub  9295  difgtsumgt  9719  zfidc  9728  gtndiv  9746  eluz2  9937  eluzsub  9962  peano2uz  9993  nn01to3  10027  divge1  10135  ledivge1le  10138  addlelt  10180  xaddass  10282  xleadd1  10288  xltadd1  10289  ixxssixx  10315  lbico1  10343  lbicc2  10397  icoshftf1o  10404  fzen  10458  fzrev3  10505  fzrevral2  10524  nelfzo  10570  elfzo0  10604  elfzo0z  10607  fzosplitprm1  10664  qbtwnre  10702  flqwordi  10738  flqword2  10739  adddivflid  10742  flltdivnn0lt  10754  modqcl  10778  mulqmod0  10782  modqmulnn  10794  modqabs2  10810  addmodid  10824  modifeq2int  10838  modqeqmodmin  10846  seqeq2  10903  seqeq3  10904  seq1g  10915  seqp1g  10918  exp3val  10993  expnegap0  10999  expgt1  11029  exprecap  11032  leexp2a  11044  expubnd  11048  sqdivap  11055  expnbnd  11116  mulsubdivbinom2ap  11165  bccmpl  11208  fihashss  11273  leisorel  11305  ccatass  11392  ccats1val2  11424  swrdval  11436  swrdval2  11439  swrdlen2  11450  swrdfv2  11451  pfxfv  11472  pfxn0  11476  pfxnd  11477  swrdswrd  11493  pfxswrd  11494  pfxpfx  11496  ccats1pfxeqbi  11530  s3cl  11574  s3fv0g  11579  s3fv1g  11580  s3fv2g  11581  shftfibg  11601  mulreap  11645  abssubne0  11874  maxleast  11996  lemininf  12018  ltmininf  12019  xrmaxltsup  12043  xrmaxaddlem  12045  xrmaxadd  12046  xrmineqinf  12054  xrltmininf  12055  xrminltinf  12057  xrminadd  12060  climuni  12078  reccn2ap  12098  isumz  12175  fsumsplitsnun  12205  geoisum1c  12306  prod1dc  12372  efltim  12484  dvdscmulr  12606  dvdsmulcr  12607  summodnegmod  12608  modmulconst  12609  dvdsmultr2  12619  dvdsexp  12647  mulmoddvds  12649  modremain  12715  divgcdz  12767  gcdaddm  12780  dvdsgcdb  12809  gcdass  12811  mulgcd  12812  gcddiv  12815  rplpwr  12823  uzwodc  12833  lcmdvdsb  12881  lcmass  12882  mulgcddvds  12891  qredeq  12893  qredeu  12894  rpmul  12895  divgcdcoprmex  12899  cncongr1  12900  rpexp  12951  rpexp12i  12953  odzcllem  13044  odzdvds  13047  odzphi  13048  pythagtriplem15  13080  pcpremul  13095  pcdiv  13104  pcqmul  13105  pcqdiv  13109  dvdsprmpweq  13137  sumhashdc  13149  pcfaclem  13151  qexpz  13154  ballotfilemfrcn0  13325  ctinf  13373  setsvala  13435  ressressg  13482  ressabsg  13483  rngbaseg  13543  ptex  13671  issubmnd  13808  ress0g  13809  imasmnd2  13812  grpasscan2  13922  grpidrcan  13923  grpidlcan  13924  grpinvadd  13936  grpsubeq0  13944  grppncan  13949  dfgrp3m  13957  grpsubpropd2  13963  imasgrp2  13966  mhmmnd  13972  mulgnegneg  13997  mulgaddcomlem  14001  mulgaddcom  14002  mulginvcom  14003  mulgmodid  14017  issubg  14029  nsgconj  14062  nsgid  14071  quselbasg  14086  quseccl0g  14087  ghmnsgima  14124  cmn4  14192  ablinvadd  14198  ablsub4  14201  abladdsub4  14202  ablpncan2  14204  gsumsncmn  14240  gsumconstcmn  14250  pwsinvg  14299  rngpropd  14338  imasrng  14339  issrg  14353  ringidss  14418  ringcom  14420  imasring  14453  unitmulcl  14504  unitmulclb  14505  dvrcl  14526  unitdvcl  14527  dvrcan1  14531  dvrcan3  14532  issubrng  14591  subrngpropd  14608  rrgeq0  14657  islmod  14711  lmodcom  14754  rmodislmodlem  14771  rmodislmod  14772  lss0cl  14790  lssvnegcl  14797  lssintclm  14805  lssincl  14806  lspss  14820  lspun  14823  lspsnvsi  14839  lsslsp  14850  rnglidlmmgm  14917  rnglidlmsgrp  14918  rnglidlrng  14919  qus2idrng  14946  qusmulrng  14953  assa2ass  15093  assa2ass2  15094  aspid  15101  aspss  15103  asclmul1  15113  asclmul2  15114  asclinvg  15116  psrbaglecl  15144  psrbagcon  15146  2basgeng  15274  clsss  15310  ntrss  15311  ntrin  15316  neiss  15342  restco  15366  restabs  15367  lmconst  15408  psmetsym  15521  psmetge0  15523  xmetge0  15557  xmetsym  15560  xmetresbl  15632  mopni3  15676  bdxmet  15693  bdmopn  15696  txmetcnp  15710  dvfvalap  15873  dvid  15887  dvidre  15889  dvcnp2cntop  15891  elplyr  15932  ply1term  15935  ptolemy  16017  logfac  16090  rpcxpadd  16102  rpmulcxp  16106  rpdivcxp  16108  cxpmul  16109  rpcxple2  16115  rpcxplt2  16116  cxpcom  16135  rplogbval  16142  rplogbcl  16143  rprelogbmulexp  16153  relogbexpap  16155  logbleb  16158  logblt  16159  rplogbcxp  16160  rpcxplogb  16161  sgmppw  16247  prmefexple  16269  lgslem1  16285  lgsfcl2  16291  lgsneg  16309  lgsne0  16323  lgssq2  16326  lgsdirnn0  16332  gausslemma2dlem1a  16343  lgsquad  16365  2lgsoddprmlem2  16391  funvtxvalg  16443  funiedgvalg  16444  lpvtx  16486  upgrex  16510  subumgredg2en  16678  iedginwlk  16764  eulerpathprum  16887  dichmul0or  16926