Theorem simp3 1026

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simpl3  1029  simpr3  1032  simp3i  1035  simp3d  1038  simp13  1056  simp23  1059  simp33  1062  3anibar  1192  3ianorr  1346  intn3an3d  1395  stoic4a  1477  stoic4b  1478  mob2  2997  sotri2  5160  sotri3  5161  feq123  5500  resasplitss  5544  fresaunres2disj  5545  sefvex  5691  ftpg  5868  fsnunf  5884  fnfvima  5921  cocan1  5960  cocan2  5961  f1oiso2  6000  riotass  6033  moriotass  6034  ovmpox  6182  ovmpoga  6183  fvmpopr2d  6190  caovimo  6248  ofrval  6277  suppvalfn  6441  fvn0elsuppb  6452  dfsmo2  6518  tfr1onlembfn  6575  tfrcllembfn  6588  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecrdg  6639  nnsucsssuc  6725  f1oen2g  6994  f1dom2g  6995  xpdom3m  7085  mapxpen  7101  diffifi  7151  unfidisj  7182  undifdc  7184  imaf1fi  7193  ssfidc  7198  sbthlemi9  7235  ctssdc  7404  endjudisj  7517  djuassen  7524  xpdjuen  7525  mulcanenq  7700  ltanqg  7715  addnnnq0  7764  nnanq0  7773  prltlu  7802  distrprg  7903  ltexprlemm  7915  recexprlem1ssl  7948  recexprlem1ssu  7949  addsrpr  8060  mulsrpr  8061  mulasssrg  8073  recexgt0sr  8088  ltpsrprg  8118  axmulass  8188  axpre-ltadd  8201  ltxrlt  8339  subadd2  8477  addsubass  8483  nppcan  8495  nppcan3  8497  subcan2  8498  subsub2  8501  subsub4  8506  pnpcan  8512  pnncan  8514  subcan  8528  subdi  8658  ltadd1  8703  leadd1  8704  leadd2  8705  ltsubadd  8706  ltsubadd2  8707  lesubadd  8708  lesubadd2  8709  ltaddsub  8710  leaddsub  8712  lesub1  8730  lesub2  8731  ltsub1  8732  ltsub2  8733  ltaddsublt  8845  gt0add  8847  reapadd1  8870  remulext1  8873  remulext2  8874  apadd2  8883  mulext2  8887  mulap0r  8889  leltap  8899  ltap  8907  apsub1  8916  divap0b  8957  divmulasscomap  8970  divcanap5  8988  dmdcanap  8996  redivclap  9005  div2negap  9009  lt2msq1  9159  ltdiv2  9161  ofnegsub  9236  nndivtr  9279  difgtsumgt  9647  gtndiv  9673  eluzsub  9884  nn01to3  9949  qdivcl  9975  irrmul  9979  rpgecl  10015  divge1  10056  xaddass  10202  xltadd1  10209  ubioog  10247  ubioc1  10262  lbico1  10263  iccleub  10264  lbicc2  10317  ubicc2  10318  icoshftf1o  10324  fzen  10377  elfz1b  10424  uznfz  10437  elfzo0  10520  elfzo0z  10523  ubmelfzo  10545  fzonn0p1p1  10558  ubmelm1fzo  10571  zsupssdc  10598  qbtwnre  10616  flqwordi  10648  flltdivnn0lt  10664  ceiqle  10675  modqval  10686  modqvalr  10687  modqcl  10688  flqpmodeq  10689  modq0  10691  mulqmod0  10692  negqmod0  10693  modqge0  10694  modqlt  10695  modqdiffl  10697  modqdifz  10698  modqmulnn  10704  modqvalp1  10705  modqabs2  10720  modqmuladdnn0  10730  qnegmod  10731  addmodid  10734  modqeqmodmin  10756  modfzo0difsn  10757  addmodlteq  10760  frec2uzf1od  10768  expnegap0  10909  expgt1  10939  exprecap  10942  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  mulbinom2  11018  expnbnd  11025  fihashss  11181  fimaxq  11194  seq3coll  11214  ccatw2s1leng  11326  ccat2s1fvwd  11335  swrdval  11340  swrdnd  11351  swrdlen2  11354  pfxn0  11380  ccatopth2  11409  s3cl  11478  s3fv0g  11483  s3fv1g  11484  s3fv2g  11485  shftfibg  11505  redivap  11559  imdivap  11566  cjdivap  11594  maxleast  11898  lemininf  11919  ltmininf  11920  bdtrilem  11924  bdtri  11925  xrmaxaddlem  11945  xrmaxadd  11946  xrmineqinf  11954  xrltmininf  11955  xrminltinf  11957  xrminadd  11960  climuni  11978  reccn2ap  11998  isumz  12075  fsumsplitsnun  12105  geoisum1c  12206  prodfap0  12231  prod1dc  12272  fprodabs  12302  cos12dec  12454  summodnegmod  12508  dvdsmultr2  12519  mulmoddvds  12549  divalglemeuneg  12609  gcdaddm  12680  gcdass  12711  mulgcd  12712  gcddiv  12715  nnminle  12731  lcmass  12782  mulgcddvds  12791  qredeq  12793  congr  12797  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  prmexpb  12848  rpexp  12850  pythagtriplem1  12963  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem15  12976  pythagtriplem19  12980  pcdiv  13000  dvdsprmpweqle  13035  sumhashdc  13045  pcbc  13049  4sqlem12  13100  4sqlem18  13106  unennn  13148  nninfdc  13204  fvsetsid  13246  ressressg  13288  rngmulrg  13351  imasaddvallemg  13528  qusaddvallemg  13546  mgmsscl  13574  plusfvalg  13576  ress0g  13656  imasmnd2  13665  imasmnd  13666  gsumfzz  13708  grpasscan2  13777  grpidrcan  13778  grpidlcan  13779  grpinvadd  13791  grppncan  13804  dfgrp3me  13813  grpsubpropd2  13818  pwsinvg  13825  imasgrp2  13827  imasgrp  13828  mhmmnd  13833  mulgnnsubcl  13851  mulgnn0subcl  13852  mulgsubcl  13853  mulgaddcomlem  13862  mulgaddcom  13863  mulgpropdg  13881  submmulg  13883  subgcl  13901  subgsubcl  13902  subgsub  13903  subgmulg  13905  nsgconj  13923  ghmsub  13968  ghmnsgima  13985  ghmeqker  13988  f1ghm0to0  13989  ablinvadd  14027  ablpncan2  14033  subgabl  14049  rngcl  14088  imasrng  14100  srgcl  14114  ringcl  14157  crngcom  14158  ringidss  14173  ringcom  14175  mulgass2  14202  imasring  14208  opprringbg  14224  unitmulcl  14258  unitmulclb  14259  dvrcl  14280  unitdvcl  14281  dvrcan1  14285  dvrcan3  14286  rhmmul  14309  subrngmcl  14354  subrgmcl  14378  subrgdv  14383  domneq0  14418  islmod  14439  scafvalg  14455  lmodcom  14481  lmodprop2d  14496  rmodislmodlem  14498  rmodislmod  14499  lsselg  14509  lssvnegcl  14524  lspss  14547  lspun  14550  lspsnvsi  14566  lsslsp  14577  sralmod  14598  lidlnegcl  14633  rspssp  14642  rnglidlrng  14646  qus2idrng  14673  zndvds  14797  psrbagaddclfi  14825  psrbagcon  14826  basgen  14945  2basgeng  14947  ntrss  14984  neiss  15015  opnneiss  15023  restco  15039  restabs  15040  cnprcl2k  15071  cnpf2  15072  lmconst  15081  cnpnei  15084  cnptoprest  15104  cnmpt2t  15158  psmetsym  15194  psmetge0  15196  xmetge0  15230  xmetsym  15233  blvalps  15253  blval  15254  ssblps  15290  ssbl  15291  blpnfctr  15304  xmssym  15334  bdxmet  15366  metcnp3  15376  dvfvalap  15546  dvid  15560  dvidre  15562  dvcnp2cntop  15564  elplyr  15605  ply1term  15608  plypow  15609  ptolemy  15689  rpcxpadd  15770  rpcxpsub  15773  rpmulcxp  15774  cxpmul  15777  rpcxple2  15783  rpcxplt2  15784  cxpcom  15803  rplogbval  15810  rplogbcl  15811  rplogbchbase  15815  rplogbreexp  15818  relogbexpap  15823  logbleb  15826  logblt  15827  rplogbcxp  15828  rpcxplogb  15829  relogbcxpbap  15830  sgmppw  15860  lgslem1  15873  lgsfvalg  15878  lgsval4  15893  lgsneg  15897  lgsne0  15911  lgsdinn0  15921  lgsquad  15953  funvtxvalg  16031  funiedgvalg  16032  upgrex  16098  uhgr2edg  16201  usgr2v1e2w  16241  subumgredg2en  16266  iedginwlk  16352  upgrwlkedg  16356  clwwlkccat  16396  clwwlknonex2  16434  eulerpathprum  16475  repiecele0  16810  repiecege0  16811  gfsumsn  16867