Theorem simp3 1001

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	|- ( ( ph /\ ps /\ ch ) -> ch )

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 998	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )
2	1	simprd 114	1 |- ( ( ph /\ ps /\ ch ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpl3  1004  simpr3  1007  simp3i  1010  simp3d  1013  simp13  1031  simp23  1034  simp33  1037  3anibar  1167  3ianorr  1320  stoic4a  1443  stoic4b  1444  mob2  2944  sotri2  5068  sotri3  5069  feq123  5402  resasplitss  5440  sefvex  5582  ftpg  5749  fsnunf  5765  fnfvima  5800  cocan1  5837  cocan2  5838  f1oiso2  5877  riotass  5908  moriotass  5909  ovmpox  6055  ovmpoga  6056  fvmpopr2d  6063  caovimo  6121  ofrval  6150  dfsmo2  6354  tfr1onlembfn  6411  tfrcllembfn  6424  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecrdg  6475  nnsucsssuc  6559  f1oen2g  6823  f1dom2g  6824  xpdom3m  6902  mapxpen  6918  diffifi  6964  unfidisj  6992  undifdc  6994  ssfidc  7007  sbthlemi9  7040  ctssdc  7188  endjudisj  7293  djuassen  7300  xpdjuen  7301  mulcanenq  7469  ltanqg  7484  addnnnq0  7533  nnanq0  7542  prltlu  7571  distrprg  7672  ltexprlemm  7684  recexprlem1ssl  7717  recexprlem1ssu  7718  addsrpr  7829  mulsrpr  7830  mulasssrg  7842  recexgt0sr  7857  ltpsrprg  7887  axmulass  7957  axpre-ltadd  7970  ltxrlt  8109  subadd2  8247  addsubass  8253  nppcan  8265  nppcan3  8267  subcan2  8268  subsub2  8271  subsub4  8276  pnpcan  8282  pnncan  8284  subcan  8298  subdi  8428  ltadd1  8473  leadd1  8474  leadd2  8475  ltsubadd  8476  ltsubadd2  8477  lesubadd  8478  lesubadd2  8479  ltaddsub  8480  leaddsub  8482  lesub1  8500  lesub2  8501  ltsub1  8502  ltsub2  8503  ltaddsublt  8615  gt0add  8617  reapadd1  8640  remulext1  8643  remulext2  8644  apadd2  8653  mulext2  8657  mulap0r  8659  leltap  8669  ltap  8677  apsub1  8686  divap0b  8727  divmulasscomap  8740  divcanap5  8758  dmdcanap  8766  redivclap  8775  div2negap  8779  lt2msq1  8929  ltdiv2  8931  ofnegsub  9006  nndivtr  9049  difgtsumgt  9412  gtndiv  9438  eluzsub  9648  nn01to3  9708  qdivcl  9734  irrmul  9738  rpgecl  9774  divge1  9815  xaddass  9961  xltadd1  9968  ubioog  10006  ubioc1  10021  lbico1  10022  iccleub  10023  lbicc2  10076  ubicc2  10077  icoshftf1o  10083  fzen  10135  elfz1b  10182  uznfz  10195  elfzo0  10275  elfzo0z  10277  ubmelfzo  10293  fzonn0p1p1  10306  ubmelm1fzo  10319  zsupssdc  10345  qbtwnre  10363  flqwordi  10395  flltdivnn0lt  10411  ceiqle  10422  modqval  10433  modqvalr  10434  modqcl  10435  flqpmodeq  10436  modq0  10438  mulqmod0  10439  negqmod0  10440  modqge0  10441  modqlt  10442  modqdiffl  10444  modqdifz  10445  modqmulnn  10451  modqvalp1  10452  modqabs2  10467  modqmuladdnn0  10477  qnegmod  10478  addmodid  10481  modqeqmodmin  10503  modfzo0difsn  10504  addmodlteq  10507  frec2uzf1od  10515  expnegap0  10656  expgt1  10686  exprecap  10689  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  mulbinom2  10765  expnbnd  10772  fihashss  10925  fimaxq  10936  seq3coll  10951  shftfibg  11002  redivap  11056  imdivap  11063  cjdivap  11091  maxleast  11395  lemininf  11416  ltmininf  11417  bdtrilem  11421  bdtri  11422  xrmaxaddlem  11442  xrmaxadd  11443  xrmineqinf  11451  xrltmininf  11452  xrminltinf  11454  xrminadd  11457  climuni  11475  reccn2ap  11495  isumz  11571  fsumsplitsnun  11601  geoisum1c  11702  prodfap0  11727  prod1dc  11768  fprodabs  11798  cos12dec  11950  summodnegmod  12004  dvdsmultr2  12015  mulmoddvds  12045  divalglemeuneg  12105  gcdaddm  12176  gcdass  12207  mulgcd  12208  gcddiv  12211  nnminle  12227  lcmass  12278  mulgcddvds  12287  qredeq  12289  congr  12293  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  prmexpb  12344  rpexp  12346  pythagtriplem1  12459  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem15  12472  pythagtriplem19  12476  pcdiv  12496  dvdsprmpweqle  12531  sumhashdc  12541  pcbc  12545  4sqlem12  12596  4sqlem18  12602  unennn  12639  nninfdc  12695  fvsetsid  12737  ressressg  12778  rngmulrg  12840  imasaddvallemg  13017  qusaddvallemg  13035  mgmsscl  13063  plusfvalg  13065  ress0g  13145  imasmnd2  13154  imasmnd  13155  gsumfzz  13197  grpasscan2  13266  grpidrcan  13267  grpidlcan  13268  grpinvadd  13280  grppncan  13293  dfgrp3me  13302  grpsubpropd2  13307  pwsinvg  13314  imasgrp2  13316  imasgrp  13317  mhmmnd  13322  mulgnnsubcl  13340  mulgnn0subcl  13341  mulgsubcl  13342  mulgaddcomlem  13351  mulgaddcom  13352  mulgpropdg  13370  submmulg  13372  subgcl  13390  subgsubcl  13391  subgsub  13392  subgmulg  13394  nsgconj  13412  ghmsub  13457  ghmnsgima  13474  ghmeqker  13477  f1ghm0to0  13478  ablinvadd  13516  ablpncan2  13522  subgabl  13538  rngcl  13576  imasrng  13588  srgcl  13602  ringcl  13645  crngcom  13646  ringidss  13661  ringcom  13663  mulgass2  13690  imasring  13696  opprringbg  13712  unitmulcl  13745  unitmulclb  13746  dvrcl  13767  unitdvcl  13768  dvrcan1  13772  dvrcan3  13773  rhmmul  13796  subrngmcl  13841  subrgmcl  13865  subrgdv  13870  domneq0  13904  islmod  13923  scafvalg  13939  lmodcom  13965  lmodprop2d  13980  rmodislmodlem  13982  rmodislmod  13983  lsselg  13993  lssvnegcl  14008  lspss  14031  lspun  14034  lspsnvsi  14050  lsslsp  14061  sralmod  14082  lidlnegcl  14117  rspssp  14126  rnglidlrng  14130  qus2idrng  14157  zndvds  14281  basgen  14400  2basgeng  14402  ntrss  14439  neiss  14470  opnneiss  14478  restco  14494  restabs  14495  cnprcl2k  14526  cnpf2  14527  lmconst  14536  cnpnei  14539  cnptoprest  14559  cnmpt2t  14613  psmetsym  14649  psmetge0  14651  xmetge0  14685  xmetsym  14688  blvalps  14708  blval  14709  ssblps  14745  ssbl  14746  blpnfctr  14759  xmssym  14789  bdxmet  14821  metcnp3  14831  dvfvalap  15001  dvid  15015  dvidre  15017  dvcnp2cntop  15019  elplyr  15060  ply1term  15063  plypow  15064  ptolemy  15144  rpcxpadd  15225  rpcxpsub  15228  rpmulcxp  15229  cxpmul  15232  rpcxple2  15238  rpcxplt2  15239  cxpcom  15258  rplogbval  15265  rplogbcl  15266  rplogbchbase  15270  rplogbreexp  15273  relogbexpap  15278  logbleb  15281  logblt  15282  rplogbcxp  15283  rpcxplogb  15284  relogbcxpbap  15285  sgmppw  15312  lgslem1  15325  lgsfvalg  15330  lgsval4  15345  lgsneg  15349  lgsne0  15363  lgsdinn0  15373  lgsquad  15405