Theorem simp1 1024

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simpl1  1027  simpr1  1030  simp1i  1033  simp1d  1036  simp11  1054  simp21  1057  simp31  1060  syld3an3  1319  3ianorr  1346  intn3an1d  1393  stoic4a  1477  stoic4b  1478  rsp2e  2584  ifnetruedc  3653  issod  4422  elirr  4645  sotri2  5141  sotri3  5142  funtpg  5388  funimaexglem  5420  feq123  5481  ftpg  5846  fsnunf  5862  foco2  5904  fcofo  5935  f1oiso2  5978  riotass  6011  ovmpox  6160  ovmpoga  6161  caovimo  6226  ofeq  6247  ofrval  6255  fvn0elsuppb  6430  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  frecsuclem  6615  frecrdg  6617  domssr  6994  mapxpen  7077  diffifi  7126  unsnfidcex  7155  unsnfidcel  7156  unfidisj  7157  undifdc  7159  ssfidc  7173  iunfidisj  7188  sbthlemi9  7207  elfir  7232  djuassen  7492  dftap2  7530  mulcanenq  7665  ltanqg  7680  addnnnq0  7729  distrlem4prl  7864  distrlem4pru  7865  distrprg  7868  aptipr  7921  addsrpr  8025  mulsrpr  8026  mulasssrg  8038  ltpsrprg  8083  axmulass  8153  axpre-ltadd  8166  mul31  8369  addsubass  8448  subcan2  8463  subsub2  8466  subsub4  8471  npncan3  8476  pnpcan  8477  pnncan  8479  subcan  8493  subdi  8623  ltadd1  8668  leadd1  8669  leadd2  8670  ltsubadd  8671  lesubadd  8673  ltaddsub  8675  leaddsub  8677  lesub1  8695  lesub2  8696  ltsub1  8697  ltsub2  8698  ltaddsublt  8810  gt0add  8812  apreap  8826  lemul1  8832  reapmul1lem  8833  reapmul1  8834  reapadd1  8835  remulext1  8838  remulext2  8839  apadd2  8848  mulext2  8852  mulap0r  8854  leltap  8864  ltap  8872  apsub1  8881  recexaplem2  8891  mulcanap  8904  mulcanap2  8905  divvalap  8913  divcanap2  8919  diveqap0  8921  divrecap  8927  divrecap2  8928  divdirap  8936  divcanap3  8937  div11ap  8939  muldivdirap  8946  divcanap5  8953  redivclap  8970  div2negap  8974  apmul1  9027  apmul2  9028  div2subap  9076  ltdiv1  9107  ltmuldiv  9113  lemuldiv  9120  lt2msq1  9124  ltdiv23  9131  lediv23  9132  squeeze0  9143  ofnegsub  9201  difgtsumgt  9610  gtndiv  9636  eluz2  9822  eluzsub  9847  peano2uz  9878  nn01to3  9912  divge1  10019  ledivge1le  10022  addlelt  10064  xaddass  10165  xleadd1  10171  xltadd1  10172  ixxssixx  10198  lbico1  10226  lbicc2  10280  icoshftf1o  10287  fzen  10340  fzrev3  10384  fzrevral2  10403  nelfzo  10449  elfzo0  10483  elfzo0z  10486  fzosplitprm1  10543  qbtwnre  10579  flqwordi  10611  flqword2  10612  adddivflid  10615  flltdivnn0lt  10627  modqcl  10651  mulqmod0  10655  modqmulnn  10667  modqabs2  10683  addmodid  10697  modifeq2int  10711  modqeqmodmin  10719  seqeq2  10776  seqeq3  10777  seq1g  10788  seqp1g  10791  exp3val  10866  expnegap0  10872  expgt1  10902  exprecap  10905  leexp2a  10917  expubnd  10921  sqdivap  10928  expnbnd  10988  mulsubdivbinom2ap  11036  bccmpl  11079  fihashss  11143  leisorel  11164  ccatass  11251  ccats1val2  11283  swrdval  11295  swrdval2  11298  swrdlen2  11309  swrdfv2  11310  pfxfv  11331  pfxn0  11335  pfxnd  11336  swrdswrd  11352  pfxswrd  11353  pfxpfx  11355  ccats1pfxeqbi  11389  s3cl  11433  s3fv0g  11438  s3fv1g  11439  s3fv2g  11440  shftfibg  11460  mulreap  11504  abssubne0  11731  maxleast  11853  lemininf  11874  ltmininf  11875  xrmaxltsup  11898  xrmaxaddlem  11900  xrmaxadd  11901  xrmineqinf  11909  xrltmininf  11910  xrminltinf  11912  xrminadd  11915  climuni  11933  reccn2ap  11953  isumz  12030  fsumsplitsnun  12060  geoisum1c  12161  prod1dc  12227  efltim  12339  dvdscmulr  12461  dvdsmulcr  12462  summodnegmod  12463  modmulconst  12464  dvdsmultr2  12474  dvdsexp  12502  mulmoddvds  12504  modremain  12570  divgcdz  12622  gcdaddm  12635  dvdsgcdb  12664  gcdass  12666  mulgcd  12667  gcddiv  12670  rplpwr  12678  uzwodc  12688  lcmdvdsb  12736  lcmass  12737  mulgcddvds  12746  qredeq  12748  qredeu  12749  rpmul  12750  divgcdcoprmex  12754  cncongr1  12755  rpexp  12805  rpexp12i  12807  odzcllem  12895  odzdvds  12898  odzphi  12899  pythagtriplem15  12931  pcpremul  12946  pcdiv  12955  pcqmul  12956  pcqdiv  12960  dvdsprmpweq  12988  sumhashdc  13000  pcfaclem  13002  qexpz  13005  ctinf  13131  setsvala  13193  ressressg  13238  ressabsg  13239  rngbaseg  13299  ptex  13427  issubmnd  13605  ress0g  13606  imasmnd2  13615  gsumfzz  13658  grpasscan2  13727  grpidrcan  13728  grpidlcan  13729  grpinvadd  13741  grpsubeq0  13749  grppncan  13754  dfgrp3m  13762  grpsubpropd2  13768  pwsinvg  13775  imasgrp2  13777  mhmmnd  13783  mulgnegneg  13808  mulgaddcomlem  13812  mulgaddcom  13813  mulginvcom  13814  mulgmodid  13828  issubg  13840  nsgconj  13873  nsgid  13882  quselbasg  13897  quseccl0g  13898  ghmnsgima  13935  cmn4  13972  ablinvadd  13977  ablsub4  13980  abladdsub4  13981  ablpncan2  13983  rngpropd  14049  imasrng  14050  issrg  14059  ringidss  14123  ringcom  14125  imasring  14158  unitmulcl  14208  unitmulclb  14209  dvrcl  14230  unitdvcl  14231  dvrcan1  14235  dvrcan3  14236  issubrng  14294  subrngpropd  14311  rrgeq0  14360  islmod  14387  lmodcom  14429  rmodislmodlem  14446  rmodislmod  14447  lss0cl  14465  lssvnegcl  14472  lssintclm  14480  lssincl  14481  lspss  14495  lspun  14498  lspsnvsi  14514  lsslsp  14525  rnglidlmmgm  14592  rnglidlmsgrp  14593  rnglidlrng  14594  qus2idrng  14621  qusmulrng  14628  psrbaglecl  14771  psrbagcon  14772  2basgeng  14893  clsss  14929  ntrss  14930  ntrin  14935  neiss  14961  restco  14985  restabs  14986  lmconst  15027  psmetsym  15140  psmetge0  15142  xmetge0  15176  xmetsym  15179  xmetresbl  15251  mopni3  15295  bdxmet  15312  bdmopn  15315  txmetcnp  15329  dvfvalap  15492  dvid  15506  dvidre  15508  dvcnp2cntop  15510  elplyr  15551  ply1term  15554  ptolemy  15635  rpcxpadd  15716  rpmulcxp  15720  rpdivcxp  15722  cxpmul  15723  rpcxple2  15729  rpcxplt2  15730  cxpcom  15749  rplogbval  15756  rplogbcl  15757  rprelogbmulexp  15767  relogbexpap  15769  logbleb  15772  logblt  15773  rplogbcxp  15774  rpcxplogb  15775  sgmppw  15806  lgslem1  15819  lgsfcl2  15825  lgsneg  15843  lgsne0  15857  lgssq2  15860  lgsdirnn0  15866  gausslemma2dlem1a  15877  lgsquad  15899  2lgsoddprmlem2  15925  funvtxvalg  15977  funiedgvalg  15978  lpvtx  16020  upgrex  16044  subumgredg2en  16212  iedginwlk  16298  eulerpathprum  16421  gfsumsn  16814