Theorem simp1 1000

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simpl1  1003  simpr1  1006  simp1i  1009  simp1d  1012  simp11  1030  simp21  1033  simp31  1036  syld3an3  1295  3ianorr  1322  intn3an1d  1368  stoic4a  1452  stoic4b  1453  rsp2e  2557  ifnetruedc  3613  issod  4367  elirr  4590  sotri2  5081  sotri3  5082  funtpg  5326  funimaexglem  5358  feq123  5419  ftpg  5770  fsnunf  5786  foco2  5824  fcofo  5855  f1oiso2  5898  riotass  5929  ovmpox  6076  ovmpoga  6077  caovimo  6142  ofeq  6163  ofrval  6171  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  frecsuclem  6494  frecrdg  6496  domssr  6871  mapxpen  6947  diffifi  6993  unsnfidcex  7019  unsnfidcel  7020  unfidisj  7021  undifdc  7023  ssfidc  7036  iunfidisj  7050  sbthlemi9  7069  elfir  7077  djuassen  7331  dftap2  7365  mulcanenq  7500  ltanqg  7515  addnnnq0  7564  distrlem4prl  7699  distrlem4pru  7700  distrprg  7703  aptipr  7756  addsrpr  7860  mulsrpr  7861  mulasssrg  7873  ltpsrprg  7918  axmulass  7988  axpre-ltadd  8001  mul31  8205  addsubass  8284  subcan2  8299  subsub2  8302  subsub4  8307  npncan3  8312  pnpcan  8313  pnncan  8315  subcan  8329  subdi  8459  ltadd1  8504  leadd1  8505  leadd2  8506  ltsubadd  8507  lesubadd  8509  ltaddsub  8511  leaddsub  8513  lesub1  8531  lesub2  8532  ltsub1  8533  ltsub2  8534  ltaddsublt  8646  gt0add  8648  apreap  8662  lemul1  8668  reapmul1lem  8669  reapmul1  8670  reapadd1  8671  remulext1  8674  remulext2  8675  apadd2  8684  mulext2  8688  mulap0r  8690  leltap  8700  ltap  8708  apsub1  8717  recexaplem2  8727  mulcanap  8740  mulcanap2  8741  divvalap  8749  divcanap2  8755  diveqap0  8757  divrecap  8763  divrecap2  8764  divdirap  8772  divcanap3  8773  div11ap  8775  muldivdirap  8782  divcanap5  8789  redivclap  8806  div2negap  8810  apmul1  8863  apmul2  8864  div2subap  8912  ltdiv1  8943  ltmuldiv  8949  lemuldiv  8956  lt2msq1  8960  ltdiv23  8967  lediv23  8968  squeeze0  8979  ofnegsub  9037  difgtsumgt  9444  gtndiv  9470  eluz2  9656  eluzsub  9680  peano2uz  9706  nn01to3  9740  divge1  9847  ledivge1le  9850  addlelt  9892  xaddass  9993  xleadd1  9999  xltadd1  10000  ixxssixx  10026  lbico1  10054  lbicc2  10108  icoshftf1o  10115  fzen  10167  fzrev3  10211  fzrevral2  10230  nelfzo  10276  elfzo0  10308  elfzo0z  10310  fzosplitprm1  10365  qbtwnre  10401  flqwordi  10433  flqword2  10434  adddivflid  10437  flltdivnn0lt  10449  modqcl  10473  mulqmod0  10477  modqmulnn  10489  modqabs2  10505  addmodid  10519  modifeq2int  10533  modqeqmodmin  10541  seqeq2  10598  seqeq3  10599  seq1g  10610  seqp1g  10613  exp3val  10688  expnegap0  10694  expgt1  10724  exprecap  10727  leexp2a  10739  expubnd  10743  sqdivap  10750  expnbnd  10810  mulsubdivbinom2ap  10858  bccmpl  10901  fihashss  10963  leisorel  10984  ccatass  11067  ccats1val2  11095  swrdval  11104  swrdval2  11107  swrdlen2  11118  swrdfv2  11119  pfxfv  11138  pfxn0  11142  pfxnd  11143  shftfibg  11164  mulreap  11208  abssubne0  11435  maxleast  11557  lemininf  11578  ltmininf  11579  xrmaxltsup  11602  xrmaxaddlem  11604  xrmaxadd  11605  xrmineqinf  11613  xrltmininf  11614  xrminltinf  11616  xrminadd  11619  climuni  11637  reccn2ap  11657  isumz  11733  fsumsplitsnun  11763  geoisum1c  11864  prod1dc  11930  efltim  12042  dvdscmulr  12164  dvdsmulcr  12165  summodnegmod  12166  modmulconst  12167  dvdsmultr2  12177  dvdsexp  12205  mulmoddvds  12207  modremain  12273  divgcdz  12325  gcdaddm  12338  dvdsgcdb  12367  gcdass  12369  mulgcd  12370  gcddiv  12373  rplpwr  12381  uzwodc  12391  lcmdvdsb  12439  lcmass  12440  mulgcddvds  12449  qredeq  12451  qredeu  12452  rpmul  12453  divgcdcoprmex  12457  cncongr1  12458  rpexp  12508  rpexp12i  12510  odzcllem  12598  odzdvds  12601  odzphi  12602  pythagtriplem15  12634  pcpremul  12649  pcdiv  12658  pcqmul  12659  pcqdiv  12663  dvdsprmpweq  12691  sumhashdc  12703  pcfaclem  12705  qexpz  12708  ctinf  12834  setsvala  12896  ressressg  12940  ressabsg  12941  rngbaseg  13001  ptex  13129  issubmnd  13307  ress0g  13308  imasmnd2  13317  gsumfzz  13360  grpasscan2  13429  grpidrcan  13430  grpidlcan  13431  grpinvadd  13443  grpsubeq0  13451  grppncan  13456  dfgrp3m  13464  grpsubpropd2  13470  pwsinvg  13477  imasgrp2  13479  mhmmnd  13485  mulgnegneg  13510  mulgaddcomlem  13514  mulgaddcom  13515  mulginvcom  13516  mulgmodid  13530  issubg  13542  nsgconj  13575  nsgid  13584  quselbasg  13599  quseccl0g  13600  ghmnsgima  13637  cmn4  13674  ablinvadd  13679  ablsub4  13682  abladdsub4  13683  ablpncan2  13685  rngpropd  13750  imasrng  13751  issrg  13760  ringidss  13824  ringcom  13826  imasring  13859  unitmulcl  13908  unitmulclb  13909  dvrcl  13930  unitdvcl  13931  dvrcan1  13935  dvrcan3  13936  issubrng  13994  subrngpropd  14011  rrgeq0  14060  islmod  14086  lmodcom  14128  rmodislmodlem  14145  rmodislmod  14146  lss0cl  14164  lssvnegcl  14171  lssintclm  14179  lssincl  14180  lspss  14194  lspun  14197  lspsnvsi  14213  lsslsp  14224  rnglidlmmgm  14291  rnglidlmsgrp  14292  rnglidlrng  14293  qus2idrng  14320  qusmulrng  14327  2basgeng  14587  clsss  14623  ntrss  14624  ntrin  14629  neiss  14655  restco  14679  restabs  14680  lmconst  14721  psmetsym  14834  psmetge0  14836  xmetge0  14870  xmetsym  14873  xmetresbl  14945  mopni3  14989  bdxmet  15006  bdmopn  15009  txmetcnp  15023  dvfvalap  15186  dvid  15200  dvidre  15202  dvcnp2cntop  15204  elplyr  15245  ply1term  15248  ptolemy  15329  rpcxpadd  15410  rpmulcxp  15414  rpdivcxp  15416  cxpmul  15417  rpcxple2  15423  rpcxplt2  15424  cxpcom  15443  rplogbval  15450  rplogbcl  15451  rprelogbmulexp  15461  relogbexpap  15463  logbleb  15466  logblt  15467  rplogbcxp  15468  rpcxplogb  15469  sgmppw  15497  lgslem1  15510  lgsfcl2  15516  lgsneg  15534  lgsne0  15548  lgssq2  15551  lgsdirnn0  15557  gausslemma2dlem1a  15568  lgsquad  15590  2lgsoddprmlem2  15616  funvtxvalg  15666  funiedgvalg  15667