Theorem simp3 999

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  simpl3  1002  simpr3  1005  simp3i  1008  simp3d  1011  simp13  1029  simp23  1032  simp33  1035  3anibar  1165  3ianorr  1309  stoic4a  1432  stoic4b  1433  mob2  2918  sotri2  5027  sotri3  5028  feq123  5358  resasplitss  5396  sefvex  5537  ftpg  5701  fsnunf  5717  fnfvima  5752  cocan1  5788  cocan2  5789  f1oiso2  5828  riotass  5858  moriotass  5859  ovmpox  6003  ovmpoga  6004  caovimo  6068  ofrval  6093  dfsmo2  6288  tfr1onlembfn  6345  tfrcllembfn  6358  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecrdg  6409  nnsucsssuc  6493  f1oen2g  6755  f1dom2g  6756  xpdom3m  6834  mapxpen  6848  diffifi  6894  unfidisj  6921  undifdc  6923  ssfidc  6934  sbthlemi9  6964  ctssdc  7112  endjudisj  7209  djuassen  7216  xpdjuen  7217  mulcanenq  7384  ltanqg  7399  addnnnq0  7448  nnanq0  7457  prltlu  7486  distrprg  7587  ltexprlemm  7599  recexprlem1ssl  7632  recexprlem1ssu  7633  addsrpr  7744  mulsrpr  7745  mulasssrg  7757  recexgt0sr  7772  ltpsrprg  7802  axmulass  7872  axpre-ltadd  7885  ltxrlt  8023  subadd2  8161  addsubass  8167  nppcan  8179  nppcan3  8181  subcan2  8182  subsub2  8185  subsub4  8190  pnpcan  8196  pnncan  8198  subcan  8212  subdi  8342  ltadd1  8386  leadd1  8387  leadd2  8388  ltsubadd  8389  ltsubadd2  8390  lesubadd  8391  lesubadd2  8392  ltaddsub  8393  leaddsub  8395  lesub1  8413  lesub2  8414  ltsub1  8415  ltsub2  8416  ltaddsublt  8528  gt0add  8530  reapadd1  8553  remulext1  8556  remulext2  8557  apadd2  8566  mulext2  8570  mulap0r  8572  leltap  8582  ltap  8590  apsub1  8599  divap0b  8640  divmulasscomap  8653  divcanap5  8671  dmdcanap  8679  redivclap  8688  div2negap  8692  lt2msq1  8842  ltdiv2  8844  nndivtr  8961  difgtsumgt  9322  gtndiv  9348  eluzsub  9557  nn01to3  9617  qdivcl  9643  irrmul  9647  rpgecl  9682  divge1  9723  xaddass  9869  xltadd1  9876  ubioog  9914  ubioc1  9929  lbico1  9930  iccleub  9931  lbicc2  9984  ubicc2  9985  icoshftf1o  9991  fzen  10043  elfz1b  10090  uznfz  10103  elfzo0  10182  elfzo0z  10184  ubmelfzo  10200  fzonn0p1p1  10213  ubmelm1fzo  10226  qbtwnre  10257  flqwordi  10288  flltdivnn0lt  10304  ceiqle  10313  modqval  10324  modqvalr  10325  modqcl  10326  flqpmodeq  10327  modq0  10329  mulqmod0  10330  negqmod0  10331  modqge0  10332  modqlt  10333  modqdiffl  10335  modqdifz  10336  modqmulnn  10342  modqvalp1  10343  modqabs2  10358  modqmuladdnn0  10368  qnegmod  10369  addmodid  10372  modqeqmodmin  10394  modfzo0difsn  10395  addmodlteq  10398  frec2uzf1od  10406  expnegap0  10528  expgt1  10558  exprecap  10561  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  mulbinom2  10637  expnbnd  10644  fihashss  10796  fimaxq  10807  seq3coll  10822  shftfibg  10829  redivap  10883  imdivap  10890  cjdivap  10918  maxleast  11222  lemininf  11242  ltmininf  11243  bdtrilem  11247  bdtri  11248  xrmaxaddlem  11268  xrmaxadd  11269  xrmineqinf  11277  xrltmininf  11278  xrminltinf  11280  xrminadd  11283  climuni  11301  reccn2ap  11321  isumz  11397  fsumsplitsnun  11427  geoisum1c  11528  prodfap0  11553  prod1dc  11594  fprodabs  11624  cos12dec  11775  summodnegmod  11829  dvdsmultr2  11840  mulmoddvds  11869  divalglemeuneg  11928  zsupssdc  11955  gcdaddm  11985  gcdass  12016  mulgcd  12017  gcddiv  12020  nnminle  12036  lcmass  12085  mulgcddvds  12094  qredeq  12096  congr  12100  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  prmexpb  12151  rpexp  12153  pythagtriplem1  12265  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem15  12278  pythagtriplem19  12282  pcdiv  12302  dvdsprmpweqle  12336  sumhashdc  12345  pcbc  12349  unennn  12398  nninfdc  12454  fvsetsid  12496  ressressg  12534  rngmulrg  12596  imasaddvallemg  12736  qusaddvallemg  12752  mgmsscl  12780  plusfvalg  12782  ress0g  12844  grpasscan2  12934  grpidrcan  12935  grpidlcan  12936  grpinvadd  12948  grppncan  12961  dfgrp3me  12970  grpsubpropd2  12975  mhmmnd  12980  mulgnnsubcl  12995  mulgnn0subcl  12996  mulgsubcl  12997  mulgaddcomlem  13006  mulgaddcom  13007  mulgpropdg  13025  subgcl  13044  subgsubcl  13045  subgsub  13046  subgmulg  13048  nsgconj  13066  ablinvadd  13113  ablpncan2  13119  srgcl  13153  ringcl  13196  crngcom  13197  ringidss  13212  ringcom  13214  mulgass2  13235  opprringbg  13250  unitmulcl  13282  unitmulclb  13283  dvrcl  13304  unitdvcl  13305  dvrcan1  13309  dvrcan3  13310  subrgmcl  13354  subrgdv  13359  islmod  13381  scafvalg  13397  lmodcom  13423  lmodprop2d  13438  rmodislmodlem  13440  rmodislmod  13441  basgen  13583  2basgeng  13585  ntrss  13622  neiss  13653  opnneiss  13661  restco  13677  restabs  13678  cnprcl2k  13709  cnpf2  13710  lmconst  13719  cnpnei  13722  cnptoprest  13742  cnmpt2t  13796  psmetsym  13832  psmetge0  13834  xmetge0  13868  xmetsym  13871  blvalps  13891  blval  13892  ssblps  13928  ssbl  13929  blpnfctr  13942  xmssym  13972  bdxmet  14004  metcnp3  14014  dvfvalap  14153  dvid  14165  dvcnp2cntop  14166  ptolemy  14248  rpcxpadd  14329  rpcxpsub  14332  rpmulcxp  14333  cxpmul  14336  rpcxple2  14341  rpcxplt2  14342  cxpcom  14360  rplogbval  14366  rplogbcl  14367  rplogbchbase  14371  rplogbreexp  14374  relogbexpap  14379  logbleb  14382  logblt  14383  rplogbcxp  14384  rpcxplogb  14385  relogbcxpbap  14386  lgslem1  14404  lgsfvalg  14409  lgsval4  14424  lgsneg  14428  lgsne0  14442  lgsdinn0  14452