Theorem simp1 1021

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simpl1  1024  simpr1  1027  simp1i  1030  simp1d  1033  simp11  1051  simp21  1054  simp31  1057  syld3an3  1316  3ianorr  1343  intn3an1d  1390  stoic4a  1474  stoic4b  1475  rsp2e  2581  ifnetruedc  3646  issod  4410  elirr  4633  sotri2  5126  sotri3  5127  funtpg  5372  funimaexglem  5404  feq123  5465  ftpg  5827  fsnunf  5843  foco2  5883  fcofo  5914  f1oiso2  5957  riotass  5990  ovmpox  6139  ovmpoga  6140  caovimo  6205  ofeq  6227  ofrval  6235  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  frecsuclem  6558  frecrdg  6560  domssr  6937  mapxpen  7017  diffifi  7064  unsnfidcex  7093  unsnfidcel  7094  unfidisj  7095  undifdc  7097  ssfidc  7110  iunfidisj  7124  sbthlemi9  7143  elfir  7151  djuassen  7410  dftap2  7448  mulcanenq  7583  ltanqg  7598  addnnnq0  7647  distrlem4prl  7782  distrlem4pru  7783  distrprg  7786  aptipr  7839  addsrpr  7943  mulsrpr  7944  mulasssrg  7956  ltpsrprg  8001  axmulass  8071  axpre-ltadd  8084  mul31  8288  addsubass  8367  subcan2  8382  subsub2  8385  subsub4  8390  npncan3  8395  pnpcan  8396  pnncan  8398  subcan  8412  subdi  8542  ltadd1  8587  leadd1  8588  leadd2  8589  ltsubadd  8590  lesubadd  8592  ltaddsub  8594  leaddsub  8596  lesub1  8614  lesub2  8615  ltsub1  8616  ltsub2  8617  ltaddsublt  8729  gt0add  8731  apreap  8745  lemul1  8751  reapmul1lem  8752  reapmul1  8753  reapadd1  8754  remulext1  8757  remulext2  8758  apadd2  8767  mulext2  8771  mulap0r  8773  leltap  8783  ltap  8791  apsub1  8800  recexaplem2  8810  mulcanap  8823  mulcanap2  8824  divvalap  8832  divcanap2  8838  diveqap0  8840  divrecap  8846  divrecap2  8847  divdirap  8855  divcanap3  8856  div11ap  8858  muldivdirap  8865  divcanap5  8872  redivclap  8889  div2negap  8893  apmul1  8946  apmul2  8947  div2subap  8995  ltdiv1  9026  ltmuldiv  9032  lemuldiv  9039  lt2msq1  9043  ltdiv23  9050  lediv23  9051  squeeze0  9062  ofnegsub  9120  difgtsumgt  9527  gtndiv  9553  eluz2  9739  eluzsub  9764  peano2uz  9790  nn01to3  9824  divge1  9931  ledivge1le  9934  addlelt  9976  xaddass  10077  xleadd1  10083  xltadd1  10084  ixxssixx  10110  lbico1  10138  lbicc2  10192  icoshftf1o  10199  fzen  10251  fzrev3  10295  fzrevral2  10314  nelfzo  10360  elfzo0  10394  elfzo0z  10396  fzosplitprm1  10452  qbtwnre  10488  flqwordi  10520  flqword2  10521  adddivflid  10524  flltdivnn0lt  10536  modqcl  10560  mulqmod0  10564  modqmulnn  10576  modqabs2  10592  addmodid  10606  modifeq2int  10620  modqeqmodmin  10628  seqeq2  10685  seqeq3  10686  seq1g  10697  seqp1g  10700  exp3val  10775  expnegap0  10781  expgt1  10811  exprecap  10814  leexp2a  10826  expubnd  10830  sqdivap  10837  expnbnd  10897  mulsubdivbinom2ap  10945  bccmpl  10988  fihashss  11051  leisorel  11072  ccatass  11156  ccats1val2  11187  swrdval  11196  swrdval2  11199  swrdlen2  11210  swrdfv2  11211  pfxfv  11232  pfxn0  11236  pfxnd  11237  swrdswrd  11253  pfxswrd  11254  pfxpfx  11256  ccats1pfxeqbi  11290  s3cl  11334  s3fv0g  11339  s3fv1g  11340  shftfibg  11347  mulreap  11391  abssubne0  11618  maxleast  11740  lemininf  11761  ltmininf  11762  xrmaxltsup  11785  xrmaxaddlem  11787  xrmaxadd  11788  xrmineqinf  11796  xrltmininf  11797  xrminltinf  11799  xrminadd  11802  climuni  11820  reccn2ap  11840  isumz  11916  fsumsplitsnun  11946  geoisum1c  12047  prod1dc  12113  efltim  12225  dvdscmulr  12347  dvdsmulcr  12348  summodnegmod  12349  modmulconst  12350  dvdsmultr2  12360  dvdsexp  12388  mulmoddvds  12390  modremain  12456  divgcdz  12508  gcdaddm  12521  dvdsgcdb  12550  gcdass  12552  mulgcd  12553  gcddiv  12556  rplpwr  12564  uzwodc  12574  lcmdvdsb  12622  lcmass  12623  mulgcddvds  12632  qredeq  12634  qredeu  12635  rpmul  12636  divgcdcoprmex  12640  cncongr1  12641  rpexp  12691  rpexp12i  12693  odzcllem  12781  odzdvds  12784  odzphi  12785  pythagtriplem15  12817  pcpremul  12832  pcdiv  12841  pcqmul  12842  pcqdiv  12846  dvdsprmpweq  12874  sumhashdc  12886  pcfaclem  12888  qexpz  12891  ctinf  13017  setsvala  13079  ressressg  13124  ressabsg  13125  rngbaseg  13185  ptex  13313  issubmnd  13491  ress0g  13492  imasmnd2  13501  gsumfzz  13544  grpasscan2  13613  grpidrcan  13614  grpidlcan  13615  grpinvadd  13627  grpsubeq0  13635  grppncan  13640  dfgrp3m  13648  grpsubpropd2  13654  pwsinvg  13661  imasgrp2  13663  mhmmnd  13669  mulgnegneg  13694  mulgaddcomlem  13698  mulgaddcom  13699  mulginvcom  13700  mulgmodid  13714  issubg  13726  nsgconj  13759  nsgid  13768  quselbasg  13783  quseccl0g  13784  ghmnsgima  13821  cmn4  13858  ablinvadd  13863  ablsub4  13866  abladdsub4  13867  ablpncan2  13869  rngpropd  13934  imasrng  13935  issrg  13944  ringidss  14008  ringcom  14010  imasring  14043  unitmulcl  14093  unitmulclb  14094  dvrcl  14115  unitdvcl  14116  dvrcan1  14120  dvrcan3  14121  issubrng  14179  subrngpropd  14196  rrgeq0  14245  islmod  14271  lmodcom  14313  rmodislmodlem  14330  rmodislmod  14331  lss0cl  14349  lssvnegcl  14356  lssintclm  14364  lssincl  14365  lspss  14379  lspun  14382  lspsnvsi  14398  lsslsp  14409  rnglidlmmgm  14476  rnglidlmsgrp  14477  rnglidlrng  14478  qus2idrng  14505  qusmulrng  14512  2basgeng  14772  clsss  14808  ntrss  14809  ntrin  14814  neiss  14840  restco  14864  restabs  14865  lmconst  14906  psmetsym  15019  psmetge0  15021  xmetge0  15055  xmetsym  15058  xmetresbl  15130  mopni3  15174  bdxmet  15191  bdmopn  15194  txmetcnp  15208  dvfvalap  15371  dvid  15385  dvidre  15387  dvcnp2cntop  15389  elplyr  15430  ply1term  15433  ptolemy  15514  rpcxpadd  15595  rpmulcxp  15599  rpdivcxp  15601  cxpmul  15602  rpcxple2  15608  rpcxplt2  15609  cxpcom  15628  rplogbval  15635  rplogbcl  15636  rprelogbmulexp  15646  relogbexpap  15648  logbleb  15651  logblt  15652  rplogbcxp  15653  rpcxplogb  15654  sgmppw  15682  lgslem1  15695  lgsfcl2  15701  lgsneg  15719  lgsne0  15733  lgssq2  15736  lgsdirnn0  15742  gausslemma2dlem1a  15753  lgsquad  15775  2lgsoddprmlem2  15801  funvtxvalg  15853  funiedgvalg  15854  lpvtx  15895  upgrex  15919  iedginwlk  16103