Theorem simp1 999

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simpl1  1002  simpr1  1005  simp1i  1008  simp1d  1011  simp11  1029  simp21  1032  simp31  1035  syld3an3  1294  3ianorr  1320  stoic4a  1443  stoic4b  1444  rsp2e  2545  ifnetruedc  3599  issod  4351  elirr  4574  sotri2  5064  sotri3  5065  funtpg  5306  funimaexglem  5338  feq123  5396  ftpg  5743  fsnunf  5759  foco2  5797  fcofo  5828  f1oiso2  5871  riotass  5902  ovmpox  6048  ovmpoga  6049  caovimo  6114  ofeq  6135  ofrval  6143  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  frecsuclem  6461  frecrdg  6463  mapxpen  6906  diffifi  6952  unsnfidcex  6978  unsnfidcel  6979  unfidisj  6980  undifdc  6982  ssfidc  6993  iunfidisj  7007  sbthlemi9  7026  elfir  7034  djuassen  7279  dftap2  7313  mulcanenq  7447  ltanqg  7462  addnnnq0  7511  distrlem4prl  7646  distrlem4pru  7647  distrprg  7650  aptipr  7703  addsrpr  7807  mulsrpr  7808  mulasssrg  7820  ltpsrprg  7865  axmulass  7935  axpre-ltadd  7948  mul31  8152  addsubass  8231  subcan2  8246  subsub2  8249  subsub4  8254  npncan3  8259  pnpcan  8260  pnncan  8262  subcan  8276  subdi  8406  ltadd1  8450  leadd1  8451  leadd2  8452  ltsubadd  8453  lesubadd  8455  ltaddsub  8457  leaddsub  8459  lesub1  8477  lesub2  8478  ltsub1  8479  ltsub2  8480  ltaddsublt  8592  gt0add  8594  apreap  8608  lemul1  8614  reapmul1lem  8615  reapmul1  8616  reapadd1  8617  remulext1  8620  remulext2  8621  apadd2  8630  mulext2  8634  mulap0r  8636  leltap  8646  ltap  8654  apsub1  8663  recexaplem2  8673  mulcanap  8686  mulcanap2  8687  divvalap  8695  divcanap2  8701  diveqap0  8703  divrecap  8709  divrecap2  8710  divdirap  8718  divcanap3  8719  div11ap  8721  muldivdirap  8728  divcanap5  8735  redivclap  8752  div2negap  8756  apmul1  8809  apmul2  8810  div2subap  8858  ltdiv1  8889  ltmuldiv  8895  lemuldiv  8902  lt2msq1  8906  ltdiv23  8913  lediv23  8914  squeeze0  8925  ofnegsub  8983  difgtsumgt  9389  gtndiv  9415  eluz2  9601  eluzsub  9625  peano2uz  9651  nn01to3  9685  divge1  9792  ledivge1le  9795  addlelt  9837  xaddass  9938  xleadd1  9944  xltadd1  9945  ixxssixx  9971  lbico1  9999  lbicc2  10053  icoshftf1o  10060  fzen  10112  fzrev3  10156  fzrevral2  10175  nelfzo  10221  elfzo0  10252  elfzo0z  10254  fzosplitprm1  10304  qbtwnre  10328  flqwordi  10360  flqword2  10361  adddivflid  10364  flltdivnn0lt  10376  modqcl  10400  mulqmod0  10404  modqmulnn  10416  modqabs2  10432  addmodid  10446  modifeq2int  10460  modqeqmodmin  10468  seqeq2  10525  seqeq3  10526  seq1g  10537  seqp1g  10540  exp3val  10615  expnegap0  10621  expgt1  10651  exprecap  10654  leexp2a  10666  expubnd  10670  sqdivap  10677  expnbnd  10737  mulsubdivbinom2ap  10785  bccmpl  10828  fihashss  10890  leisorel  10911  shftfibg  10967  mulreap  11011  abssubne0  11238  maxleast  11360  lemininf  11380  ltmininf  11381  xrmaxltsup  11404  xrmaxaddlem  11406  xrmaxadd  11407  xrmineqinf  11415  xrltmininf  11416  xrminltinf  11418  xrminadd  11421  climuni  11439  reccn2ap  11459  isumz  11535  fsumsplitsnun  11565  geoisum1c  11666  prod1dc  11732  efltim  11844  dvdscmulr  11966  dvdsmulcr  11967  summodnegmod  11968  modmulconst  11969  dvdsmultr2  11979  dvdsexp  12006  mulmoddvds  12008  modremain  12073  divgcdz  12111  gcdaddm  12124  dvdsgcdb  12153  gcdass  12155  mulgcd  12156  gcddiv  12159  rplpwr  12167  uzwodc  12177  lcmdvdsb  12225  lcmass  12226  mulgcddvds  12235  qredeq  12237  qredeu  12238  rpmul  12239  divgcdcoprmex  12243  cncongr1  12244  rpexp  12294  rpexp12i  12296  odzcllem  12383  odzdvds  12386  odzphi  12387  pythagtriplem15  12419  pcpremul  12434  pcdiv  12443  pcqmul  12444  pcqdiv  12448  dvdsprmpweq  12476  sumhashdc  12488  pcfaclem  12490  qexpz  12493  ctinf  12590  setsvala  12652  ressressg  12696  ressabsg  12697  rngbaseg  12756  ptex  12878  issubmnd  13026  ress0g  13027  gsumfzz  13070  grpasscan2  13139  grpidrcan  13140  grpidlcan  13141  grpinvadd  13153  grpsubeq0  13161  grppncan  13166  dfgrp3m  13174  grpsubpropd2  13180  imasgrp2  13183  mhmmnd  13189  mulgnegneg  13214  mulgaddcomlem  13218  mulgaddcom  13219  mulginvcom  13220  mulgmodid  13234  issubg  13246  nsgconj  13279  nsgid  13288  quselbasg  13303  quseccl0g  13304  ghmnsgima  13341  cmn4  13378  ablinvadd  13383  ablsub4  13386  abladdsub4  13387  ablpncan2  13389  rngpropd  13454  imasrng  13455  issrg  13464  ringidss  13528  ringcom  13530  imasring  13563  unitmulcl  13612  unitmulclb  13613  dvrcl  13634  unitdvcl  13635  dvrcan1  13639  dvrcan3  13640  issubrng  13698  subrngpropd  13715  rrgeq0  13764  islmod  13790  lmodcom  13832  rmodislmodlem  13849  rmodislmod  13850  lss0cl  13868  lssvnegcl  13875  lssintclm  13883  lssincl  13884  lspss  13898  lspun  13901  lspsnvsi  13917  lsslsp  13928  rnglidlmmgm  13995  rnglidlmsgrp  13996  rnglidlrng  13997  qus2idrng  14024  qusmulrng  14031  2basgeng  14261  clsss  14297  ntrss  14298  ntrin  14303  neiss  14329  restco  14353  restabs  14354  lmconst  14395  psmetsym  14508  psmetge0  14510  xmetge0  14544  xmetsym  14547  xmetresbl  14619  mopni3  14663  bdxmet  14680  bdmopn  14683  txmetcnp  14697  dvfvalap  14860  dvid  14874  dvidre  14876  dvcnp2cntop  14878  elplyr  14919  ply1term  14922  ptolemy  15000  rpcxpadd  15081  rpmulcxp  15085  rpdivcxp  15087  cxpmul  15088  rpcxple2  15093  rpcxplt2  15094  cxpcom  15112  rplogbval  15118  rplogbcl  15119  rprelogbmulexp  15129  relogbexpap  15131  logbleb  15134  logblt  15135  rplogbcxp  15136  rpcxplogb  15137  lgslem1  15157  lgsfcl2  15163  lgsneg  15181  lgsne0  15195  lgssq2  15198  lgsdirnn0  15204  gausslemma2dlem1a  15215  lgsquad  15237  2lgsoddprmlem2  15263