Theorem simp3 1023

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simpl3  1026  simpr3  1029  simp3i  1032  simp3d  1035  simp13  1053  simp23  1056  simp33  1059  3anibar  1189  3ianorr  1343  intn3an3d  1392  stoic4a  1474  stoic4b  1475  mob2  2983  sotri2  5125  sotri3  5126  feq123  5464  resasplitss  5504  sefvex  5647  ftpg  5822  fsnunf  5838  fnfvima  5873  cocan1  5910  cocan2  5911  f1oiso2  5950  riotass  5983  moriotass  5984  ovmpox  6132  ovmpoga  6133  fvmpopr2d  6140  caovimo  6198  ofrval  6227  dfsmo2  6431  tfr1onlembfn  6488  tfrcllembfn  6501  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecrdg  6552  nnsucsssuc  6636  f1oen2g  6904  f1dom2g  6905  xpdom3m  6989  mapxpen  7005  diffifi  7052  unfidisj  7080  undifdc  7082  ssfidc  7095  sbthlemi9  7128  ctssdc  7276  endjudisj  7388  djuassen  7395  xpdjuen  7396  mulcanenq  7568  ltanqg  7583  addnnnq0  7632  nnanq0  7641  prltlu  7670  distrprg  7771  ltexprlemm  7783  recexprlem1ssl  7816  recexprlem1ssu  7817  addsrpr  7928  mulsrpr  7929  mulasssrg  7941  recexgt0sr  7956  ltpsrprg  7986  axmulass  8056  axpre-ltadd  8069  ltxrlt  8208  subadd2  8346  addsubass  8352  nppcan  8364  nppcan3  8366  subcan2  8367  subsub2  8370  subsub4  8375  pnpcan  8381  pnncan  8383  subcan  8397  subdi  8527  ltadd1  8572  leadd1  8573  leadd2  8574  ltsubadd  8575  ltsubadd2  8576  lesubadd  8577  lesubadd2  8578  ltaddsub  8579  leaddsub  8581  lesub1  8599  lesub2  8600  ltsub1  8601  ltsub2  8602  ltaddsublt  8714  gt0add  8716  reapadd1  8739  remulext1  8742  remulext2  8743  apadd2  8752  mulext2  8756  mulap0r  8758  leltap  8768  ltap  8776  apsub1  8785  divap0b  8826  divmulasscomap  8839  divcanap5  8857  dmdcanap  8865  redivclap  8874  div2negap  8878  lt2msq1  9028  ltdiv2  9030  ofnegsub  9105  nndivtr  9148  difgtsumgt  9512  gtndiv  9538  eluzsub  9748  nn01to3  9808  qdivcl  9834  irrmul  9838  rpgecl  9874  divge1  9915  xaddass  10061  xltadd1  10068  ubioog  10106  ubioc1  10121  lbico1  10122  iccleub  10123  lbicc2  10176  ubicc2  10177  icoshftf1o  10183  fzen  10235  elfz1b  10282  uznfz  10295  elfzo0  10378  elfzo0z  10380  ubmelfzo  10401  fzonn0p1p1  10414  ubmelm1fzo  10427  zsupssdc  10453  qbtwnre  10471  flqwordi  10503  flltdivnn0lt  10519  ceiqle  10530  modqval  10541  modqvalr  10542  modqcl  10543  flqpmodeq  10544  modq0  10546  mulqmod0  10547  negqmod0  10548  modqge0  10549  modqlt  10550  modqdiffl  10552  modqdifz  10553  modqmulnn  10559  modqvalp1  10560  modqabs2  10575  modqmuladdnn0  10585  qnegmod  10586  addmodid  10589  modqeqmodmin  10611  modfzo0difsn  10612  addmodlteq  10615  frec2uzf1od  10623  expnegap0  10764  expgt1  10794  exprecap  10797  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  mulbinom2  10873  expnbnd  10880  fihashss  11033  fimaxq  11044  seq3coll  11059  swrdval  11175  swrdnd  11186  swrdlen2  11189  pfxn0  11215  ccatopth2  11244  s3cl  11313  s3fv0g  11318  s3fv1g  11319  shftfibg  11326  redivap  11380  imdivap  11387  cjdivap  11415  maxleast  11719  lemininf  11740  ltmininf  11741  bdtrilem  11745  bdtri  11746  xrmaxaddlem  11766  xrmaxadd  11767  xrmineqinf  11775  xrltmininf  11776  xrminltinf  11778  xrminadd  11781  climuni  11799  reccn2ap  11819  isumz  11895  fsumsplitsnun  11925  geoisum1c  12026  prodfap0  12051  prod1dc  12092  fprodabs  12122  cos12dec  12274  summodnegmod  12328  dvdsmultr2  12339  mulmoddvds  12369  divalglemeuneg  12429  gcdaddm  12500  gcdass  12531  mulgcd  12532  gcddiv  12535  nnminle  12551  lcmass  12602  mulgcddvds  12611  qredeq  12613  congr  12617  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  prmexpb  12668  rpexp  12670  pythagtriplem1  12783  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem15  12796  pythagtriplem19  12800  pcdiv  12820  dvdsprmpweqle  12855  sumhashdc  12865  pcbc  12869  4sqlem12  12920  4sqlem18  12926  unennn  12963  nninfdc  13019  fvsetsid  13061  ressressg  13103  rngmulrg  13166  imasaddvallemg  13343  qusaddvallemg  13361  mgmsscl  13389  plusfvalg  13391  ress0g  13471  imasmnd2  13480  imasmnd  13481  gsumfzz  13523  grpasscan2  13592  grpidrcan  13593  grpidlcan  13594  grpinvadd  13606  grppncan  13619  dfgrp3me  13628  grpsubpropd2  13633  pwsinvg  13640  imasgrp2  13642  imasgrp  13643  mhmmnd  13648  mulgnnsubcl  13666  mulgnn0subcl  13667  mulgsubcl  13668  mulgaddcomlem  13677  mulgaddcom  13678  mulgpropdg  13696  submmulg  13698  subgcl  13716  subgsubcl  13717  subgsub  13718  subgmulg  13720  nsgconj  13738  ghmsub  13783  ghmnsgima  13800  ghmeqker  13803  f1ghm0to0  13804  ablinvadd  13842  ablpncan2  13848  subgabl  13864  rngcl  13902  imasrng  13914  srgcl  13928  ringcl  13971  crngcom  13972  ringidss  13987  ringcom  13989  mulgass2  14016  imasring  14022  opprringbg  14038  unitmulcl  14071  unitmulclb  14072  dvrcl  14093  unitdvcl  14094  dvrcan1  14098  dvrcan3  14099  rhmmul  14122  subrngmcl  14167  subrgmcl  14191  subrgdv  14196  domneq0  14230  islmod  14249  scafvalg  14265  lmodcom  14291  lmodprop2d  14306  rmodislmodlem  14308  rmodislmod  14309  lsselg  14319  lssvnegcl  14334  lspss  14357  lspun  14360  lspsnvsi  14376  lsslsp  14387  sralmod  14408  lidlnegcl  14443  rspssp  14452  rnglidlrng  14456  qus2idrng  14483  zndvds  14607  basgen  14748  2basgeng  14750  ntrss  14787  neiss  14818  opnneiss  14826  restco  14842  restabs  14843  cnprcl2k  14874  cnpf2  14875  lmconst  14884  cnpnei  14887  cnptoprest  14907  cnmpt2t  14961  psmetsym  14997  psmetge0  14999  xmetge0  15033  xmetsym  15036  blvalps  15056  blval  15057  ssblps  15093  ssbl  15094  blpnfctr  15107  xmssym  15137  bdxmet  15169  metcnp3  15179  dvfvalap  15349  dvid  15363  dvidre  15365  dvcnp2cntop  15367  elplyr  15408  ply1term  15411  plypow  15412  ptolemy  15492  rpcxpadd  15573  rpcxpsub  15576  rpmulcxp  15577  cxpmul  15580  rpcxple2  15586  rpcxplt2  15587  cxpcom  15606  rplogbval  15613  rplogbcl  15614  rplogbchbase  15618  rplogbreexp  15621  relogbexpap  15626  logbleb  15629  logblt  15630  rplogbcxp  15631  rpcxplogb  15632  relogbcxpbap  15633  sgmppw  15660  lgslem1  15673  lgsfvalg  15678  lgsval4  15693  lgsneg  15697  lgsne0  15711  lgsdinn0  15721  lgsquad  15753  funvtxvalg  15831  funiedgvalg  15832  upgrex  15897  uhgr2edg  15998