Theorem simp1 997

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  simpl1  1000  simpr1  1003  simp1i  1006  simp1d  1009  simp11  1027  simp21  1030  simp31  1033  syld3an3  1283  3ianorr  1309  stoic4a  1432  stoic4b  1433  rsp2e  2528  issod  4321  elirr  4542  sotri2  5028  sotri3  5029  funtpg  5269  funimaexglem  5301  feq123  5359  ftpg  5702  fsnunf  5718  foco2  5756  fcofo  5787  f1oiso2  5830  riotass  5860  ovmpox  6005  ovmpoga  6006  caovimo  6070  ofeq  6087  ofrval  6095  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  frecsuclem  6409  frecrdg  6411  mapxpen  6850  diffifi  6896  unsnfidcex  6921  unsnfidcel  6922  unfidisj  6923  undifdc  6925  ssfidc  6936  iunfidisj  6947  sbthlemi9  6966  elfir  6974  djuassen  7218  dftap2  7252  mulcanenq  7386  ltanqg  7401  addnnnq0  7450  distrlem4prl  7585  distrlem4pru  7586  distrprg  7589  aptipr  7642  addsrpr  7746  mulsrpr  7747  mulasssrg  7759  ltpsrprg  7804  axmulass  7874  axpre-ltadd  7887  mul31  8090  addsubass  8169  subcan2  8184  subsub2  8187  subsub4  8192  npncan3  8197  pnpcan  8198  pnncan  8200  subcan  8214  subdi  8344  ltadd1  8388  leadd1  8389  leadd2  8390  ltsubadd  8391  lesubadd  8393  ltaddsub  8395  leaddsub  8397  lesub1  8415  lesub2  8416  ltsub1  8417  ltsub2  8418  ltaddsublt  8530  gt0add  8532  apreap  8546  lemul1  8552  reapmul1lem  8553  reapmul1  8554  reapadd1  8555  remulext1  8558  remulext2  8559  apadd2  8568  mulext2  8572  mulap0r  8574  leltap  8584  ltap  8592  apsub1  8601  recexaplem2  8611  mulcanap  8624  mulcanap2  8625  divvalap  8633  divcanap2  8639  diveqap0  8641  divrecap  8647  divrecap2  8648  divdirap  8656  divcanap3  8657  div11ap  8659  muldivdirap  8666  divcanap5  8673  redivclap  8690  div2negap  8694  apmul1  8747  apmul2  8748  div2subap  8796  ltdiv1  8827  ltmuldiv  8833  lemuldiv  8840  lt2msq1  8844  ltdiv23  8851  lediv23  8852  squeeze0  8863  difgtsumgt  9324  gtndiv  9350  eluz2  9536  eluzsub  9559  peano2uz  9585  nn01to3  9619  divge1  9725  ledivge1le  9728  addlelt  9770  xaddass  9871  xleadd1  9877  xltadd1  9878  ixxssixx  9904  lbico1  9932  lbicc2  9986  icoshftf1o  9993  fzen  10045  fzrev3  10089  fzrevral2  10108  elfzo0  10184  elfzo0z  10186  fzosplitprm1  10236  qbtwnre  10259  flqwordi  10290  flqword2  10291  adddivflid  10294  flltdivnn0lt  10306  modqcl  10328  mulqmod0  10332  modqmulnn  10344  modqabs2  10360  addmodid  10374  modifeq2int  10388  modqeqmodmin  10396  seqeq2  10451  seqeq3  10452  exp3val  10524  expnegap0  10530  expgt1  10560  exprecap  10563  leexp2a  10575  expubnd  10579  sqdivap  10586  expnbnd  10646  mulsubdivbinom2ap  10693  bccmpl  10736  fihashss  10798  leisorel  10819  shftfibg  10831  mulreap  10875  abssubne0  11102  maxleast  11224  lemininf  11244  ltmininf  11245  xrmaxltsup  11268  xrmaxaddlem  11270  xrmaxadd  11271  xrmineqinf  11279  xrltmininf  11280  xrminltinf  11282  xrminadd  11285  climuni  11303  reccn2ap  11323  isumz  11399  fsumsplitsnun  11429  geoisum1c  11530  prod1dc  11596  efltim  11708  dvdscmulr  11829  dvdsmulcr  11830  summodnegmod  11831  modmulconst  11832  dvdsmultr2  11842  dvdsexp  11869  mulmoddvds  11871  modremain  11936  divgcdz  11974  gcdaddm  11987  dvdsgcdb  12016  gcdass  12018  mulgcd  12019  gcddiv  12022  rplpwr  12030  uzwodc  12040  lcmdvdsb  12086  lcmass  12087  mulgcddvds  12096  qredeq  12098  qredeu  12099  rpmul  12100  divgcdcoprmex  12104  cncongr1  12105  rpexp  12155  rpexp12i  12157  odzcllem  12244  odzdvds  12247  odzphi  12248  pythagtriplem15  12280  pcpremul  12295  pcdiv  12304  pcqmul  12305  pcqdiv  12309  dvdsprmpweq  12336  sumhashdc  12347  pcfaclem  12349  qexpz  12352  ctinf  12433  setsvala  12495  ressressg  12536  ressabsg  12537  rngbaseg  12596  ptex  12718  issubmnd  12848  ress0g  12849  grpasscan2  12939  grpidrcan  12940  grpidlcan  12941  grpinvadd  12953  grpsubeq0  12961  grppncan  12966  dfgrp3m  12974  grpsubpropd2  12980  mhmmnd  12985  mulgnegneg  13007  mulgaddcomlem  13011  mulgaddcom  13012  mulginvcom  13013  mulgmodid  13027  issubg  13038  nsgconj  13071  nsgid  13080  cmn4  13113  ablinvadd  13118  ablsub4  13121  abladdsub4  13122  ablpncan2  13124  issrg  13153  ringidss  13217  ringcom  13219  unitmulcl  13287  unitmulclb  13288  dvrcl  13309  unitdvcl  13310  dvrcan1  13314  dvrcan3  13315  islmod  13386  lmodcom  13428  rmodislmodlem  13445  rmodislmod  13446  lss0cl  13460  lssvnegcl  13468  lssintclm  13476  lssincl  13477  lspss  13490  lspun  13493  lspsnvsi  13509  lsslsp  13520  2basgeng  13667  clsss  13703  ntrss  13704  ntrin  13709  neiss  13735  restco  13759  restabs  13760  lmconst  13801  psmetsym  13914  psmetge0  13916  xmetge0  13950  xmetsym  13953  xmetresbl  14025  mopni3  14069  bdxmet  14086  bdmopn  14089  txmetcnp  14103  dvfvalap  14235  dvid  14247  dvcnp2cntop  14248  ptolemy  14330  rpcxpadd  14411  rpmulcxp  14415  rpdivcxp  14417  cxpmul  14418  rpcxple2  14423  rpcxplt2  14424  cxpcom  14442  rplogbval  14448  rplogbcl  14449  rprelogbmulexp  14459  relogbexpap  14461  logbleb  14464  logblt  14465  rplogbcxp  14466  rpcxplogb  14467  lgslem1  14486  lgsfcl2  14492  lgsneg  14510  lgsne0  14524  lgssq2  14527  lgsdirnn0  14533  2lgsoddprmlem2  14539