Theorem simp3 1001

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simpl3  1004  simpr3  1007  simp3i  1010  simp3d  1013  simp13  1031  simp23  1034  simp33  1037  3anibar  1167  3ianorr  1321  intn3an3d  1369  stoic4a  1451  stoic4b  1452  mob2  2952  sotri2  5079  sotri3  5080  feq123  5416  resasplitss  5454  sefvex  5596  ftpg  5767  fsnunf  5783  fnfvima  5818  cocan1  5855  cocan2  5856  f1oiso2  5895  riotass  5926  moriotass  5927  ovmpox  6073  ovmpoga  6074  fvmpopr2d  6081  caovimo  6139  ofrval  6168  dfsmo2  6372  tfr1onlembfn  6429  tfrcllembfn  6442  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecrdg  6493  nnsucsssuc  6577  f1oen2g  6845  f1dom2g  6846  xpdom3m  6928  mapxpen  6944  diffifi  6990  unfidisj  7018  undifdc  7020  ssfidc  7033  sbthlemi9  7066  ctssdc  7214  endjudisj  7321  djuassen  7328  xpdjuen  7329  mulcanenq  7497  ltanqg  7512  addnnnq0  7561  nnanq0  7570  prltlu  7599  distrprg  7700  ltexprlemm  7712  recexprlem1ssl  7745  recexprlem1ssu  7746  addsrpr  7857  mulsrpr  7858  mulasssrg  7870  recexgt0sr  7885  ltpsrprg  7915  axmulass  7985  axpre-ltadd  7998  ltxrlt  8137  subadd2  8275  addsubass  8281  nppcan  8293  nppcan3  8295  subcan2  8296  subsub2  8299  subsub4  8304  pnpcan  8310  pnncan  8312  subcan  8326  subdi  8456  ltadd1  8501  leadd1  8502  leadd2  8503  ltsubadd  8504  ltsubadd2  8505  lesubadd  8506  lesubadd2  8507  ltaddsub  8508  leaddsub  8510  lesub1  8528  lesub2  8529  ltsub1  8530  ltsub2  8531  ltaddsublt  8643  gt0add  8645  reapadd1  8668  remulext1  8671  remulext2  8672  apadd2  8681  mulext2  8685  mulap0r  8687  leltap  8697  ltap  8705  apsub1  8714  divap0b  8755  divmulasscomap  8768  divcanap5  8786  dmdcanap  8794  redivclap  8803  div2negap  8807  lt2msq1  8957  ltdiv2  8959  ofnegsub  9034  nndivtr  9077  difgtsumgt  9441  gtndiv  9467  eluzsub  9677  nn01to3  9737  qdivcl  9763  irrmul  9767  rpgecl  9803  divge1  9844  xaddass  9990  xltadd1  9997  ubioog  10035  ubioc1  10050  lbico1  10051  iccleub  10052  lbicc2  10105  ubicc2  10106  icoshftf1o  10112  fzen  10164  elfz1b  10211  uznfz  10224  elfzo0  10304  elfzo0z  10306  ubmelfzo  10327  fzonn0p1p1  10340  ubmelm1fzo  10353  zsupssdc  10379  qbtwnre  10397  flqwordi  10429  flltdivnn0lt  10445  ceiqle  10456  modqval  10467  modqvalr  10468  modqcl  10469  flqpmodeq  10470  modq0  10472  mulqmod0  10473  negqmod0  10474  modqge0  10475  modqlt  10476  modqdiffl  10478  modqdifz  10479  modqmulnn  10485  modqvalp1  10486  modqabs2  10501  modqmuladdnn0  10511  qnegmod  10512  addmodid  10515  modqeqmodmin  10537  modfzo0difsn  10538  addmodlteq  10541  frec2uzf1od  10549  expnegap0  10690  expgt1  10720  exprecap  10723  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  mulbinom2  10799  expnbnd  10806  fihashss  10959  fimaxq  10970  seq3coll  10985  shftfibg  11102  redivap  11156  imdivap  11163  cjdivap  11191  maxleast  11495  lemininf  11516  ltmininf  11517  bdtrilem  11521  bdtri  11522  xrmaxaddlem  11542  xrmaxadd  11543  xrmineqinf  11551  xrltmininf  11552  xrminltinf  11554  xrminadd  11557  climuni  11575  reccn2ap  11595  isumz  11671  fsumsplitsnun  11701  geoisum1c  11802  prodfap0  11827  prod1dc  11868  fprodabs  11898  cos12dec  12050  summodnegmod  12104  dvdsmultr2  12115  mulmoddvds  12145  divalglemeuneg  12205  gcdaddm  12276  gcdass  12307  mulgcd  12308  gcddiv  12311  nnminle  12327  lcmass  12378  mulgcddvds  12387  qredeq  12389  congr  12393  divgcdcoprmex  12395  cncongr1  12396  cncongr2  12397  prmexpb  12444  rpexp  12446  pythagtriplem1  12559  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem12  12569  pythagtriplem13  12570  pythagtriplem15  12572  pythagtriplem19  12576  pcdiv  12596  dvdsprmpweqle  12631  sumhashdc  12641  pcbc  12645  4sqlem12  12696  4sqlem18  12702  unennn  12739  nninfdc  12795  fvsetsid  12837  ressressg  12878  rngmulrg  12941  imasaddvallemg  13118  qusaddvallemg  13136  mgmsscl  13164  plusfvalg  13166  ress0g  13246  imasmnd2  13255  imasmnd  13256  gsumfzz  13298  grpasscan2  13367  grpidrcan  13368  grpidlcan  13369  grpinvadd  13381  grppncan  13394  dfgrp3me  13403  grpsubpropd2  13408  pwsinvg  13415  imasgrp2  13417  imasgrp  13418  mhmmnd  13423  mulgnnsubcl  13441  mulgnn0subcl  13442  mulgsubcl  13443  mulgaddcomlem  13452  mulgaddcom  13453  mulgpropdg  13471  submmulg  13473  subgcl  13491  subgsubcl  13492  subgsub  13493  subgmulg  13495  nsgconj  13513  ghmsub  13558  ghmnsgima  13575  ghmeqker  13578  f1ghm0to0  13579  ablinvadd  13617  ablpncan2  13623  subgabl  13639  rngcl  13677  imasrng  13689  srgcl  13703  ringcl  13746  crngcom  13747  ringidss  13762  ringcom  13764  mulgass2  13791  imasring  13797  opprringbg  13813  unitmulcl  13846  unitmulclb  13847  dvrcl  13868  unitdvcl  13869  dvrcan1  13873  dvrcan3  13874  rhmmul  13897  subrngmcl  13942  subrgmcl  13966  subrgdv  13971  domneq0  14005  islmod  14024  scafvalg  14040  lmodcom  14066  lmodprop2d  14081  rmodislmodlem  14083  rmodislmod  14084  lsselg  14094  lssvnegcl  14109  lspss  14132  lspun  14135  lspsnvsi  14151  lsslsp  14162  sralmod  14183  lidlnegcl  14218  rspssp  14227  rnglidlrng  14231  qus2idrng  14258  zndvds  14382  basgen  14523  2basgeng  14525  ntrss  14562  neiss  14593  opnneiss  14601  restco  14617  restabs  14618  cnprcl2k  14649  cnpf2  14650  lmconst  14659  cnpnei  14662  cnptoprest  14682  cnmpt2t  14736  psmetsym  14772  psmetge0  14774  xmetge0  14808  xmetsym  14811  blvalps  14831  blval  14832  ssblps  14868  ssbl  14869  blpnfctr  14882  xmssym  14912  bdxmet  14944  metcnp3  14954  dvfvalap  15124  dvid  15138  dvidre  15140  dvcnp2cntop  15142  elplyr  15183  ply1term  15186  plypow  15187  ptolemy  15267  rpcxpadd  15348  rpcxpsub  15351  rpmulcxp  15352  cxpmul  15355  rpcxple2  15361  rpcxplt2  15362  cxpcom  15381  rplogbval  15388  rplogbcl  15389  rplogbchbase  15393  rplogbreexp  15396  relogbexpap  15401  logbleb  15404  logblt  15405  rplogbcxp  15406  rpcxplogb  15407  relogbcxpbap  15408  sgmppw  15435  lgslem1  15448  lgsfvalg  15453  lgsval4  15468  lgsneg  15472  lgsne0  15486  lgsdinn0  15496  lgsquad  15528  funvtxvalg  15604  funiedgvalg  15605