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  3000  sotri2  5165  sotri3  5166  feq123  5505  resasplitss  5549  fresaunres2disj  5550  sefvex  5696  ftpg  5873  fsnunf  5889  fnfvima  5926  cocan1  5966  cocan2  5967  f1oiso2  6006  riotass  6041  moriotass  6042  ovmpox  6190  ovmpoga  6191  fvmpopr2d  6198  caovimo  6256  ofrval  6286  suppvalfn  6454  fvn0elsuppb  6465  dfsmo2  6531  tfr1onlembfn  6588  tfrcllembfn  6601  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecrdg  6652  nnsucsssuc  6738  f1oen2g  7007  f1dom2g  7008  xpdom3m  7098  mapxpen  7114  diffifi  7164  unfidisj  7195  undifdc  7197  imaf1fi  7206  ssfidc  7211  sbthlemi9  7248  ctssdc  7417  endjudisj  7530  djuassen  7537  xpdjuen  7538  mulcanenq  7716  ltanqg  7731  addnnnq0  7780  nnanq0  7789  prltlu  7818  distrprg  7919  ltexprlemm  7931  recexprlem1ssl  7964  recexprlem1ssu  7965  addsrpr  8076  mulsrpr  8077  mulasssrg  8089  recexgt0sr  8104  ltpsrprg  8134  axmulass  8204  axpre-ltadd  8217  ltxrlt  8355  subadd2  8493  addsubass  8499  nppcan  8511  nppcan3  8513  subcan2  8514  subsub2  8517  subsub4  8522  pnpcan  8528  pnncan  8530  subcan  8544  subdi  8675  ltadd1  8720  leadd1  8721  leadd2  8722  ltsubadd  8723  ltsubadd2  8724  lesubadd  8725  lesubadd2  8726  ltaddsub  8727  leaddsub  8729  lesub1  8747  lesub2  8748  ltsub1  8749  ltsub2  8750  ltaddsublt  8862  gt0add  8864  reapadd1  8887  remulext1  8890  remulext2  8891  apadd2  8900  mulext2  8904  mulap0r  8906  leltap  8916  ltap  8924  apsub1  8933  divap0b  8974  divmulasscomap  8987  divcanap5  9005  dmdcanap  9013  redivclap  9022  div2negap  9026  lt2msq1  9176  ltdiv2  9178  ofnegsub  9253  nndivtr  9296  difgtsumgt  9664  zfidc  9673  gtndiv  9691  eluzsub  9902  nn01to3  9967  qdivcl  9993  irrmul  9997  rpgecl  10033  divge1  10074  xaddass  10221  xltadd1  10228  ubioog  10266  ubioc1  10281  lbico1  10282  iccleub  10283  lbicc2  10336  ubicc2  10337  icoshftf1o  10343  fzen  10397  elfz1b  10446  uznfz  10459  elfzo0  10542  elfzo0z  10545  ubmelfzo  10567  fzonn0p1p1  10580  ubmelm1fzo  10593  zsupssdc  10622  qbtwnre  10640  flqwordi  10672  flltdivnn0lt  10688  ceiqle  10699  modqval  10710  modqvalr  10711  modqcl  10712  flqpmodeq  10713  modq0  10715  mulqmod0  10716  negqmod0  10717  modqge0  10718  modqlt  10719  modqdiffl  10721  modqdifz  10722  modqmulnn  10728  modqvalp1  10729  modqabs2  10744  modqmuladdnn0  10754  qnegmod  10755  addmodid  10758  modqeqmodmin  10780  modfzo0difsn  10781  addmodlteq  10784  frec2uzf1od  10792  expnegap0  10933  expgt1  10963  exprecap  10966  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  mulbinom2  11042  expnbnd  11050  fihashss  11206  fimaxq  11219  seq3coll  11239  ccatw2s1leng  11351  ccat2s1fvwd  11360  swrdval  11365  swrdnd  11376  swrdlen2  11379  pfxn0  11405  ccatopth2  11434  s3cl  11503  s3fv0g  11508  s3fv1g  11509  s3fv2g  11510  shftfibg  11530  redivap  11584  imdivap  11591  cjdivap  11619  maxleast  11923  lemininf  11944  ltmininf  11945  bdtrilem  11949  bdtri  11950  xrmaxaddlem  11970  xrmaxadd  11971  xrmineqinf  11979  xrltmininf  11980  xrminltinf  11982  xrminadd  11985  climuni  12003  reccn2ap  12023  isumz  12100  fsumsplitsnun  12130  geoisum1c  12231  prodfap0  12256  prod1dc  12297  fprodabs  12327  cos12dec  12479  summodnegmod  12533  dvdsmultr2  12544  mulmoddvds  12574  divalglemeuneg  12634  gcdaddm  12705  gcdass  12736  mulgcd  12737  gcddiv  12740  nnminle  12756  lcmass  12807  mulgcddvds  12816  qredeq  12818  congr  12822  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  prmexpb  12873  rpexp  12875  pythagtriplem1  12988  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem15  13001  pythagtriplem19  13005  pcdiv  13025  dvdsprmpweqle  13060  sumhashdc  13070  pcbc  13074  4sqlem12  13125  4sqlem18  13131  ballotfilemsgt1  13198  ballotfilemfrcn0  13217  unennn  13232  nninfdc  13288  fvsetsid  13330  ressressg  13372  rngmulrg  13435  imasaddvallemg  13579  qusaddvallemg  13597  mgmsscl  13624  plusfvalg  13626  ress0g  13704  imasmnd2  13707  imasmnd  13708  gsumfzz  13750  grpasscan2  13819  grpidrcan  13820  grpidlcan  13821  grpinvadd  13833  grppncan  13846  dfgrp3me  13855  grpsubpropd2  13860  imasgrp2  13863  imasgrp  13864  mhmmnd  13869  mulgnnsubcl  13887  mulgnn0subcl  13888  mulgsubcl  13889  mulgaddcomlem  13898  mulgaddcom  13899  mulgpropdg  13917  submmulg  13919  subgcl  13937  subgsubcl  13938  subgsub  13939  subgmulg  13941  nsgconj  13959  ghmsub  14004  ghmnsgima  14021  ghmeqker  14024  f1ghm0to0  14025  ablinvadd  14063  ablpncan2  14069  subgabl  14085  gfsumsn  14107  pwsinvg  14157  rngcl  14183  imasrng  14195  rng1zrlem  14198  srgcl  14213  ringcl  14256  crngcom  14257  ringidss  14272  ringcom  14274  mulgass2  14301  imasring  14307  opprringbg  14323  unitmulcl  14358  unitmulclb  14359  dvrcl  14380  unitdvcl  14381  dvrcan1  14385  dvrcan3  14386  rhmmul  14409  subrngmcl  14455  subrgmcl  14479  subrgdv  14484  domneq0  14519  islmod  14565  scafvalg  14581  lmodcom  14607  lmodprop2d  14622  rmodislmodlem  14624  rmodislmod  14625  lsselg  14635  lssvnegcl  14650  lspss  14673  lspun  14676  lspsnvsi  14692  lsslsp  14703  sralmod  14724  lidlnegcl  14759  rspssp  14768  rnglidlrng  14772  qus2idrng  14799  zndvds  14923  psrbagaddclfi  14951  psrbagcon  14952  basgen  15071  2basgeng  15073  ntrss  15110  neiss  15141  opnneiss  15149  restco  15165  restabs  15166  cnprcl2k  15197  cnpf2  15198  lmconst  15207  cnpnei  15210  cnptoprest  15230  cnmpt2t  15284  psmetsym  15320  psmetge0  15322  xmetge0  15356  xmetsym  15359  blvalps  15379  blval  15380  ssblps  15416  ssbl  15417  blpnfctr  15430  xmssym  15460  bdxmet  15492  metcnp3  15502  dvfvalap  15672  dvid  15686  dvidre  15688  dvcnp2cntop  15690  elplyr  15731  ply1term  15734  plypow  15735  ptolemy  15815  rpcxpadd  15896  rpcxpsub  15899  rpmulcxp  15900  cxpmul  15903  rpcxple2  15909  rpcxplt2  15910  cxpcom  15929  rplogbval  15936  rplogbcl  15937  rplogbchbase  15941  rplogbreexp  15944  relogbexpap  15949  logbleb  15952  logblt  15953  rplogbcxp  15954  rpcxplogb  15955  relogbcxpbap  15956  sgmppw  15986  lgslem1  15999  lgsfvalg  16004  lgsval4  16019  lgsneg  16023  lgsne0  16037  lgsdinn0  16047  lgsquad  16079  funvtxvalg  16157  funiedgvalg  16158  upgrex  16224  uhgr2edg  16327  usgr2v1e2w  16367  subumgredg2en  16392  iedginwlk  16478  upgrwlkedg  16482  clwwlkccat  16522  clwwlknonex2  16560  eulerpathprum  16601  repiecele0  16936  repiecege0  16937