Theorem simp3 1002

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simpl3  1005  simpr3  1008  simp3i  1011  simp3d  1014  simp13  1032  simp23  1035  simp33  1038  3anibar  1168  3ianorr  1322  intn3an3d  1370  stoic4a  1452  stoic4b  1453  mob2  2960  sotri2  5099  sotri3  5100  feq123  5437  resasplitss  5477  sefvex  5620  ftpg  5791  fsnunf  5807  fnfvima  5842  cocan1  5879  cocan2  5880  f1oiso2  5919  riotass  5950  moriotass  5951  ovmpox  6097  ovmpoga  6098  fvmpopr2d  6105  caovimo  6163  ofrval  6192  dfsmo2  6396  tfr1onlembfn  6453  tfrcllembfn  6466  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecrdg  6517  nnsucsssuc  6601  f1oen2g  6869  f1dom2g  6870  xpdom3m  6954  mapxpen  6970  diffifi  7017  unfidisj  7045  undifdc  7047  ssfidc  7060  sbthlemi9  7093  ctssdc  7241  endjudisj  7353  djuassen  7360  xpdjuen  7361  mulcanenq  7533  ltanqg  7548  addnnnq0  7597  nnanq0  7606  prltlu  7635  distrprg  7736  ltexprlemm  7748  recexprlem1ssl  7781  recexprlem1ssu  7782  addsrpr  7893  mulsrpr  7894  mulasssrg  7906  recexgt0sr  7921  ltpsrprg  7951  axmulass  8021  axpre-ltadd  8034  ltxrlt  8173  subadd2  8311  addsubass  8317  nppcan  8329  nppcan3  8331  subcan2  8332  subsub2  8335  subsub4  8340  pnpcan  8346  pnncan  8348  subcan  8362  subdi  8492  ltadd1  8537  leadd1  8538  leadd2  8539  ltsubadd  8540  ltsubadd2  8541  lesubadd  8542  lesubadd2  8543  ltaddsub  8544  leaddsub  8546  lesub1  8564  lesub2  8565  ltsub1  8566  ltsub2  8567  ltaddsublt  8679  gt0add  8681  reapadd1  8704  remulext1  8707  remulext2  8708  apadd2  8717  mulext2  8721  mulap0r  8723  leltap  8733  ltap  8741  apsub1  8750  divap0b  8791  divmulasscomap  8804  divcanap5  8822  dmdcanap  8830  redivclap  8839  div2negap  8843  lt2msq1  8993  ltdiv2  8995  ofnegsub  9070  nndivtr  9113  difgtsumgt  9477  gtndiv  9503  eluzsub  9713  nn01to3  9773  qdivcl  9799  irrmul  9803  rpgecl  9839  divge1  9880  xaddass  10026  xltadd1  10033  ubioog  10071  ubioc1  10086  lbico1  10087  iccleub  10088  lbicc2  10141  ubicc2  10142  icoshftf1o  10148  fzen  10200  elfz1b  10247  uznfz  10260  elfzo0  10343  elfzo0z  10345  ubmelfzo  10366  fzonn0p1p1  10379  ubmelm1fzo  10392  zsupssdc  10418  qbtwnre  10436  flqwordi  10468  flltdivnn0lt  10484  ceiqle  10495  modqval  10506  modqvalr  10507  modqcl  10508  flqpmodeq  10509  modq0  10511  mulqmod0  10512  negqmod0  10513  modqge0  10514  modqlt  10515  modqdiffl  10517  modqdifz  10518  modqmulnn  10524  modqvalp1  10525  modqabs2  10540  modqmuladdnn0  10550  qnegmod  10551  addmodid  10554  modqeqmodmin  10576  modfzo0difsn  10577  addmodlteq  10580  frec2uzf1od  10588  expnegap0  10729  expgt1  10759  exprecap  10762  expaddzaplem  10764  expaddzap  10765  expmulzap  10767  mulbinom2  10838  expnbnd  10845  fihashss  10998  fimaxq  11009  seq3coll  11024  swrdval  11139  swrdnd  11150  swrdlen2  11153  pfxn0  11179  ccatopth2  11208  shftfibg  11246  redivap  11300  imdivap  11307  cjdivap  11335  maxleast  11639  lemininf  11660  ltmininf  11661  bdtrilem  11665  bdtri  11666  xrmaxaddlem  11686  xrmaxadd  11687  xrmineqinf  11695  xrltmininf  11696  xrminltinf  11698  xrminadd  11701  climuni  11719  reccn2ap  11739  isumz  11815  fsumsplitsnun  11845  geoisum1c  11946  prodfap0  11971  prod1dc  12012  fprodabs  12042  cos12dec  12194  summodnegmod  12248  dvdsmultr2  12259  mulmoddvds  12289  divalglemeuneg  12349  gcdaddm  12420  gcdass  12451  mulgcd  12452  gcddiv  12455  nnminle  12471  lcmass  12522  mulgcddvds  12531  qredeq  12533  congr  12537  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  prmexpb  12588  rpexp  12590  pythagtriplem1  12703  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem15  12716  pythagtriplem19  12720  pcdiv  12740  dvdsprmpweqle  12775  sumhashdc  12785  pcbc  12789  4sqlem12  12840  4sqlem18  12846  unennn  12883  nninfdc  12939  fvsetsid  12981  ressressg  13022  rngmulrg  13085  imasaddvallemg  13262  qusaddvallemg  13280  mgmsscl  13308  plusfvalg  13310  ress0g  13390  imasmnd2  13399  imasmnd  13400  gsumfzz  13442  grpasscan2  13511  grpidrcan  13512  grpidlcan  13513  grpinvadd  13525  grppncan  13538  dfgrp3me  13547  grpsubpropd2  13552  pwsinvg  13559  imasgrp2  13561  imasgrp  13562  mhmmnd  13567  mulgnnsubcl  13585  mulgnn0subcl  13586  mulgsubcl  13587  mulgaddcomlem  13596  mulgaddcom  13597  mulgpropdg  13615  submmulg  13617  subgcl  13635  subgsubcl  13636  subgsub  13637  subgmulg  13639  nsgconj  13657  ghmsub  13702  ghmnsgima  13719  ghmeqker  13722  f1ghm0to0  13723  ablinvadd  13761  ablpncan2  13767  subgabl  13783  rngcl  13821  imasrng  13833  srgcl  13847  ringcl  13890  crngcom  13891  ringidss  13906  ringcom  13908  mulgass2  13935  imasring  13941  opprringbg  13957  unitmulcl  13990  unitmulclb  13991  dvrcl  14012  unitdvcl  14013  dvrcan1  14017  dvrcan3  14018  rhmmul  14041  subrngmcl  14086  subrgmcl  14110  subrgdv  14115  domneq0  14149  islmod  14168  scafvalg  14184  lmodcom  14210  lmodprop2d  14225  rmodislmodlem  14227  rmodislmod  14228  lsselg  14238  lssvnegcl  14253  lspss  14276  lspun  14279  lspsnvsi  14295  lsslsp  14306  sralmod  14327  lidlnegcl  14362  rspssp  14371  rnglidlrng  14375  qus2idrng  14402  zndvds  14526  basgen  14667  2basgeng  14669  ntrss  14706  neiss  14737  opnneiss  14745  restco  14761  restabs  14762  cnprcl2k  14793  cnpf2  14794  lmconst  14803  cnpnei  14806  cnptoprest  14826  cnmpt2t  14880  psmetsym  14916  psmetge0  14918  xmetge0  14952  xmetsym  14955  blvalps  14975  blval  14976  ssblps  15012  ssbl  15013  blpnfctr  15026  xmssym  15056  bdxmet  15088  metcnp3  15098  dvfvalap  15268  dvid  15282  dvidre  15284  dvcnp2cntop  15286  elplyr  15327  ply1term  15330  plypow  15331  ptolemy  15411  rpcxpadd  15492  rpcxpsub  15495  rpmulcxp  15496  cxpmul  15499  rpcxple2  15505  rpcxplt2  15506  cxpcom  15525  rplogbval  15532  rplogbcl  15533  rplogbchbase  15537  rplogbreexp  15540  relogbexpap  15545  logbleb  15548  logblt  15549  rplogbcxp  15550  rpcxplogb  15551  relogbcxpbap  15552  sgmppw  15579  lgslem1  15592  lgsfvalg  15597  lgsval4  15612  lgsneg  15616  lgsne0  15630  lgsdinn0  15640  lgsquad  15672  funvtxvalg  15750  funiedgvalg  15751  upgrex  15814