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  2559  ifnetruedc  3623  issod  4384  elirr  4607  sotri2  5099  sotri3  5100  funtpg  5344  funimaexglem  5376  feq123  5437  ftpg  5791  fsnunf  5807  foco2  5845  fcofo  5876  f1oiso2  5919  riotass  5950  ovmpox  6097  ovmpoga  6098  caovimo  6163  ofeq  6184  ofrval  6192  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  frecsuclem  6515  frecrdg  6517  domssr  6892  mapxpen  6970  diffifi  7017  unsnfidcex  7043  unsnfidcel  7044  unfidisj  7045  undifdc  7047  ssfidc  7060  iunfidisj  7074  sbthlemi9  7093  elfir  7101  djuassen  7360  dftap2  7398  mulcanenq  7533  ltanqg  7548  addnnnq0  7597  distrlem4prl  7732  distrlem4pru  7733  distrprg  7736  aptipr  7789  addsrpr  7893  mulsrpr  7894  mulasssrg  7906  ltpsrprg  7951  axmulass  8021  axpre-ltadd  8034  mul31  8238  addsubass  8317  subcan2  8332  subsub2  8335  subsub4  8340  npncan3  8345  pnpcan  8346  pnncan  8348  subcan  8362  subdi  8492  ltadd1  8537  leadd1  8538  leadd2  8539  ltsubadd  8540  lesubadd  8542  ltaddsub  8544  leaddsub  8546  lesub1  8564  lesub2  8565  ltsub1  8566  ltsub2  8567  ltaddsublt  8679  gt0add  8681  apreap  8695  lemul1  8701  reapmul1lem  8702  reapmul1  8703  reapadd1  8704  remulext1  8707  remulext2  8708  apadd2  8717  mulext2  8721  mulap0r  8723  leltap  8733  ltap  8741  apsub1  8750  recexaplem2  8760  mulcanap  8773  mulcanap2  8774  divvalap  8782  divcanap2  8788  diveqap0  8790  divrecap  8796  divrecap2  8797  divdirap  8805  divcanap3  8806  div11ap  8808  muldivdirap  8815  divcanap5  8822  redivclap  8839  div2negap  8843  apmul1  8896  apmul2  8897  div2subap  8945  ltdiv1  8976  ltmuldiv  8982  lemuldiv  8989  lt2msq1  8993  ltdiv23  9000  lediv23  9001  squeeze0  9012  ofnegsub  9070  difgtsumgt  9477  gtndiv  9503  eluz2  9689  eluzsub  9713  peano2uz  9739  nn01to3  9773  divge1  9880  ledivge1le  9883  addlelt  9925  xaddass  10026  xleadd1  10032  xltadd1  10033  ixxssixx  10059  lbico1  10087  lbicc2  10141  icoshftf1o  10148  fzen  10200  fzrev3  10244  fzrevral2  10263  nelfzo  10309  elfzo0  10343  elfzo0z  10345  fzosplitprm1  10400  qbtwnre  10436  flqwordi  10468  flqword2  10469  adddivflid  10472  flltdivnn0lt  10484  modqcl  10508  mulqmod0  10512  modqmulnn  10524  modqabs2  10540  addmodid  10554  modifeq2int  10568  modqeqmodmin  10576  seqeq2  10633  seqeq3  10634  seq1g  10645  seqp1g  10648  exp3val  10723  expnegap0  10729  expgt1  10759  exprecap  10762  leexp2a  10774  expubnd  10778  sqdivap  10785  expnbnd  10845  mulsubdivbinom2ap  10893  bccmpl  10936  fihashss  10998  leisorel  11019  ccatass  11102  ccats1val2  11130  swrdval  11139  swrdval2  11142  swrdlen2  11153  swrdfv2  11154  pfxfv  11175  pfxn0  11179  pfxnd  11180  swrdswrd  11196  pfxswrd  11197  pfxpfx  11199  ccats1pfxeqbi  11233  shftfibg  11246  mulreap  11290  abssubne0  11517  maxleast  11639  lemininf  11660  ltmininf  11661  xrmaxltsup  11684  xrmaxaddlem  11686  xrmaxadd  11687  xrmineqinf  11695  xrltmininf  11696  xrminltinf  11698  xrminadd  11701  climuni  11719  reccn2ap  11739  isumz  11815  fsumsplitsnun  11845  geoisum1c  11946  prod1dc  12012  efltim  12124  dvdscmulr  12246  dvdsmulcr  12247  summodnegmod  12248  modmulconst  12249  dvdsmultr2  12259  dvdsexp  12287  mulmoddvds  12289  modremain  12355  divgcdz  12407  gcdaddm  12420  dvdsgcdb  12449  gcdass  12451  mulgcd  12452  gcddiv  12455  rplpwr  12463  uzwodc  12473  lcmdvdsb  12521  lcmass  12522  mulgcddvds  12531  qredeq  12533  qredeu  12534  rpmul  12535  divgcdcoprmex  12539  cncongr1  12540  rpexp  12590  rpexp12i  12592  odzcllem  12680  odzdvds  12683  odzphi  12684  pythagtriplem15  12716  pcpremul  12731  pcdiv  12740  pcqmul  12741  pcqdiv  12745  dvdsprmpweq  12773  sumhashdc  12785  pcfaclem  12787  qexpz  12790  ctinf  12916  setsvala  12978  ressressg  13022  ressabsg  13023  rngbaseg  13083  ptex  13211  issubmnd  13389  ress0g  13390  imasmnd2  13399  gsumfzz  13442  grpasscan2  13511  grpidrcan  13512  grpidlcan  13513  grpinvadd  13525  grpsubeq0  13533  grppncan  13538  dfgrp3m  13546  grpsubpropd2  13552  pwsinvg  13559  imasgrp2  13561  mhmmnd  13567  mulgnegneg  13592  mulgaddcomlem  13596  mulgaddcom  13597  mulginvcom  13598  mulgmodid  13612  issubg  13624  nsgconj  13657  nsgid  13666  quselbasg  13681  quseccl0g  13682  ghmnsgima  13719  cmn4  13756  ablinvadd  13761  ablsub4  13764  abladdsub4  13765  ablpncan2  13767  rngpropd  13832  imasrng  13833  issrg  13842  ringidss  13906  ringcom  13908  imasring  13941  unitmulcl  13990  unitmulclb  13991  dvrcl  14012  unitdvcl  14013  dvrcan1  14017  dvrcan3  14018  issubrng  14076  subrngpropd  14093  rrgeq0  14142  islmod  14168  lmodcom  14210  rmodislmodlem  14227  rmodislmod  14228  lss0cl  14246  lssvnegcl  14253  lssintclm  14261  lssincl  14262  lspss  14276  lspun  14279  lspsnvsi  14295  lsslsp  14306  rnglidlmmgm  14373  rnglidlmsgrp  14374  rnglidlrng  14375  qus2idrng  14402  qusmulrng  14409  2basgeng  14669  clsss  14705  ntrss  14706  ntrin  14711  neiss  14737  restco  14761  restabs  14762  lmconst  14803  psmetsym  14916  psmetge0  14918  xmetge0  14952  xmetsym  14955  xmetresbl  15027  mopni3  15071  bdxmet  15088  bdmopn  15091  txmetcnp  15105  dvfvalap  15268  dvid  15282  dvidre  15284  dvcnp2cntop  15286  elplyr  15327  ply1term  15330  ptolemy  15411  rpcxpadd  15492  rpmulcxp  15496  rpdivcxp  15498  cxpmul  15499  rpcxple2  15505  rpcxplt2  15506  cxpcom  15525  rplogbval  15532  rplogbcl  15533  rprelogbmulexp  15543  relogbexpap  15545  logbleb  15548  logblt  15549  rplogbcxp  15550  rpcxplogb  15551  sgmppw  15579  lgslem1  15592  lgsfcl2  15598  lgsneg  15616  lgsne0  15630  lgssq2  15633  lgsdirnn0  15639  gausslemma2dlem1a  15650  lgsquad  15672  2lgsoddprmlem2  15698  funvtxvalg  15750  funiedgvalg  15751  lpvtx  15790  upgrex  15814