Theorem simp3 1025

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simpl3  1028  simpr3  1031  simp3i  1034  simp3d  1037  simp13  1055  simp23  1058  simp33  1061  3anibar  1191  3ianorr  1345  intn3an3d  1394  stoic4a  1476  stoic4b  1477  mob2  2986  sotri2  5134  sotri3  5135  feq123  5474  resasplitss  5516  sefvex  5660  ftpg  5838  fsnunf  5854  fnfvima  5889  cocan1  5928  cocan2  5929  f1oiso2  5968  riotass  6001  moriotass  6002  ovmpox  6150  ovmpoga  6151  fvmpopr2d  6158  caovimo  6216  ofrval  6246  dfsmo2  6453  tfr1onlembfn  6510  tfrcllembfn  6523  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecrdg  6574  nnsucsssuc  6660  f1oen2g  6928  f1dom2g  6929  xpdom3m  7018  mapxpen  7034  diffifi  7083  unfidisj  7114  undifdc  7116  imaf1fi  7125  ssfidc  7130  sbthlemi9  7164  ctssdc  7312  endjudisj  7425  djuassen  7432  xpdjuen  7433  mulcanenq  7605  ltanqg  7620  addnnnq0  7669  nnanq0  7678  prltlu  7707  distrprg  7808  ltexprlemm  7820  recexprlem1ssl  7853  recexprlem1ssu  7854  addsrpr  7965  mulsrpr  7966  mulasssrg  7978  recexgt0sr  7993  ltpsrprg  8023  axmulass  8093  axpre-ltadd  8106  ltxrlt  8245  subadd2  8383  addsubass  8389  nppcan  8401  nppcan3  8403  subcan2  8404  subsub2  8407  subsub4  8412  pnpcan  8418  pnncan  8420  subcan  8434  subdi  8564  ltadd1  8609  leadd1  8610  leadd2  8611  ltsubadd  8612  ltsubadd2  8613  lesubadd  8614  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  ltaddsublt  8751  gt0add  8753  reapadd1  8776  remulext1  8779  remulext2  8780  apadd2  8789  mulext2  8793  mulap0r  8795  leltap  8805  ltap  8813  apsub1  8822  divap0b  8863  divmulasscomap  8876  divcanap5  8894  dmdcanap  8902  redivclap  8911  div2negap  8915  lt2msq1  9065  ltdiv2  9067  ofnegsub  9142  nndivtr  9185  difgtsumgt  9549  gtndiv  9575  eluzsub  9786  nn01to3  9851  qdivcl  9877  irrmul  9881  rpgecl  9917  divge1  9958  xaddass  10104  xltadd1  10111  ubioog  10149  ubioc1  10164  lbico1  10165  iccleub  10166  lbicc2  10219  ubicc2  10220  icoshftf1o  10226  fzen  10278  elfz1b  10325  uznfz  10338  elfzo0  10421  elfzo0z  10424  ubmelfzo  10446  fzonn0p1p1  10459  ubmelm1fzo  10472  zsupssdc  10499  qbtwnre  10517  flqwordi  10549  flltdivnn0lt  10565  ceiqle  10576  modqval  10587  modqvalr  10588  modqcl  10589  flqpmodeq  10590  modq0  10592  mulqmod0  10593  negqmod0  10594  modqge0  10595  modqlt  10596  modqdiffl  10598  modqdifz  10599  modqmulnn  10605  modqvalp1  10606  modqabs2  10621  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  modqeqmodmin  10657  modfzo0difsn  10658  addmodlteq  10661  frec2uzf1od  10669  expnegap0  10810  expgt1  10840  exprecap  10843  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  mulbinom2  10919  expnbnd  10926  fihashss  11081  fimaxq  11092  seq3coll  11107  ccatw2s1leng  11219  ccat2s1fvwd  11228  swrdval  11233  swrdnd  11244  swrdlen2  11247  pfxn0  11273  ccatopth2  11302  s3cl  11371  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  shftfibg  11398  redivap  11452  imdivap  11459  cjdivap  11487  maxleast  11791  lemininf  11812  ltmininf  11813  bdtrilem  11817  bdtri  11818  xrmaxaddlem  11838  xrmaxadd  11839  xrmineqinf  11847  xrltmininf  11848  xrminltinf  11850  xrminadd  11853  climuni  11871  reccn2ap  11891  isumz  11968  fsumsplitsnun  11998  geoisum1c  12099  prodfap0  12124  prod1dc  12165  fprodabs  12195  cos12dec  12347  summodnegmod  12401  dvdsmultr2  12412  mulmoddvds  12442  divalglemeuneg  12502  gcdaddm  12573  gcdass  12604  mulgcd  12605  gcddiv  12608  nnminle  12624  lcmass  12675  mulgcddvds  12684  qredeq  12686  congr  12690  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  prmexpb  12741  rpexp  12743  pythagtriplem1  12856  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem15  12869  pythagtriplem19  12873  pcdiv  12893  dvdsprmpweqle  12928  sumhashdc  12938  pcbc  12942  4sqlem12  12993  4sqlem18  12999  unennn  13036  nninfdc  13092  fvsetsid  13134  ressressg  13176  rngmulrg  13239  imasaddvallemg  13416  qusaddvallemg  13434  mgmsscl  13462  plusfvalg  13464  ress0g  13544  imasmnd2  13553  imasmnd  13554  gsumfzz  13596  grpasscan2  13665  grpidrcan  13666  grpidlcan  13667  grpinvadd  13679  grppncan  13692  dfgrp3me  13701  grpsubpropd2  13706  pwsinvg  13713  imasgrp2  13715  imasgrp  13716  mhmmnd  13721  mulgnnsubcl  13739  mulgnn0subcl  13740  mulgsubcl  13741  mulgaddcomlem  13750  mulgaddcom  13751  mulgpropdg  13769  submmulg  13771  subgcl  13789  subgsubcl  13790  subgsub  13791  subgmulg  13793  nsgconj  13811  ghmsub  13856  ghmnsgima  13873  ghmeqker  13876  f1ghm0to0  13877  ablinvadd  13915  ablpncan2  13921  subgabl  13937  rngcl  13976  imasrng  13988  srgcl  14002  ringcl  14045  crngcom  14046  ringidss  14061  ringcom  14063  mulgass2  14090  imasring  14096  opprringbg  14112  unitmulcl  14146  unitmulclb  14147  dvrcl  14168  unitdvcl  14169  dvrcan1  14173  dvrcan3  14174  rhmmul  14197  subrngmcl  14242  subrgmcl  14266  subrgdv  14271  domneq0  14305  islmod  14324  scafvalg  14340  lmodcom  14366  lmodprop2d  14381  rmodislmodlem  14383  rmodislmod  14384  lsselg  14394  lssvnegcl  14409  lspss  14432  lspun  14435  lspsnvsi  14451  lsslsp  14462  sralmod  14483  lidlnegcl  14518  rspssp  14527  rnglidlrng  14531  qus2idrng  14558  zndvds  14682  basgen  14823  2basgeng  14825  ntrss  14862  neiss  14893  opnneiss  14901  restco  14917  restabs  14918  cnprcl2k  14949  cnpf2  14950  lmconst  14959  cnpnei  14962  cnptoprest  14982  cnmpt2t  15036  psmetsym  15072  psmetge0  15074  xmetge0  15108  xmetsym  15111  blvalps  15131  blval  15132  ssblps  15168  ssbl  15169  blpnfctr  15182  xmssym  15212  bdxmet  15244  metcnp3  15254  dvfvalap  15424  dvid  15438  dvidre  15440  dvcnp2cntop  15442  elplyr  15483  ply1term  15486  plypow  15487  ptolemy  15567  rpcxpadd  15648  rpcxpsub  15651  rpmulcxp  15652  cxpmul  15655  rpcxple2  15661  rpcxplt2  15662  cxpcom  15681  rplogbval  15688  rplogbcl  15689  rplogbchbase  15693  rplogbreexp  15696  relogbexpap  15701  logbleb  15704  logblt  15705  rplogbcxp  15706  rpcxplogb  15707  relogbcxpbap  15708  sgmppw  15735  lgslem1  15748  lgsfvalg  15753  lgsval4  15768  lgsneg  15772  lgsne0  15786  lgsdinn0  15796  lgsquad  15828  funvtxvalg  15906  funiedgvalg  15907  upgrex  15973  uhgr2edg  16076  usgr2v1e2w  16116  subumgredg2en  16141  iedginwlk  16227  upgrwlkedg  16231  clwwlkccat  16271  clwwlknonex2  16309  eulerpathprum  16350  gfsumsn  16737