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  2953  sotri2  5080  sotri3  5081  feq123  5417  resasplitss  5455  sefvex  5597  ftpg  5768  fsnunf  5784  fnfvima  5819  cocan1  5856  cocan2  5857  f1oiso2  5896  riotass  5927  moriotass  5928  ovmpox  6074  ovmpoga  6075  fvmpopr2d  6082  caovimo  6140  ofrval  6169  dfsmo2  6373  tfr1onlembfn  6430  tfrcllembfn  6443  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecrdg  6494  nnsucsssuc  6578  f1oen2g  6846  f1dom2g  6847  xpdom3m  6929  mapxpen  6945  diffifi  6991  unfidisj  7019  undifdc  7021  ssfidc  7034  sbthlemi9  7067  ctssdc  7215  endjudisj  7322  djuassen  7329  xpdjuen  7330  mulcanenq  7498  ltanqg  7513  addnnnq0  7562  nnanq0  7571  prltlu  7600  distrprg  7701  ltexprlemm  7713  recexprlem1ssl  7746  recexprlem1ssu  7747  addsrpr  7858  mulsrpr  7859  mulasssrg  7871  recexgt0sr  7886  ltpsrprg  7916  axmulass  7986  axpre-ltadd  7999  ltxrlt  8138  subadd2  8276  addsubass  8282  nppcan  8294  nppcan3  8296  subcan2  8297  subsub2  8300  subsub4  8305  pnpcan  8311  pnncan  8313  subcan  8327  subdi  8457  ltadd1  8502  leadd1  8503  leadd2  8504  ltsubadd  8505  ltsubadd2  8506  lesubadd  8507  lesubadd2  8508  ltaddsub  8509  leaddsub  8511  lesub1  8529  lesub2  8530  ltsub1  8531  ltsub2  8532  ltaddsublt  8644  gt0add  8646  reapadd1  8669  remulext1  8672  remulext2  8673  apadd2  8682  mulext2  8686  mulap0r  8688  leltap  8698  ltap  8706  apsub1  8715  divap0b  8756  divmulasscomap  8769  divcanap5  8787  dmdcanap  8795  redivclap  8804  div2negap  8808  lt2msq1  8958  ltdiv2  8960  ofnegsub  9035  nndivtr  9078  difgtsumgt  9442  gtndiv  9468  eluzsub  9678  nn01to3  9738  qdivcl  9764  irrmul  9768  rpgecl  9804  divge1  9845  xaddass  9991  xltadd1  9998  ubioog  10036  ubioc1  10051  lbico1  10052  iccleub  10053  lbicc2  10106  ubicc2  10107  icoshftf1o  10113  fzen  10165  elfz1b  10212  uznfz  10225  elfzo0  10306  elfzo0z  10308  ubmelfzo  10329  fzonn0p1p1  10342  ubmelm1fzo  10355  zsupssdc  10381  qbtwnre  10399  flqwordi  10431  flltdivnn0lt  10447  ceiqle  10458  modqval  10469  modqvalr  10470  modqcl  10471  flqpmodeq  10472  modq0  10474  mulqmod0  10475  negqmod0  10476  modqge0  10477  modqlt  10478  modqdiffl  10480  modqdifz  10481  modqmulnn  10487  modqvalp1  10488  modqabs2  10503  modqmuladdnn0  10513  qnegmod  10514  addmodid  10517  modqeqmodmin  10539  modfzo0difsn  10540  addmodlteq  10543  frec2uzf1od  10551  expnegap0  10692  expgt1  10722  exprecap  10725  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  mulbinom2  10801  expnbnd  10808  fihashss  10961  fimaxq  10972  seq3coll  10987  swrdval  11101  swrdnd  11112  swrdlen2  11115  shftfibg  11131  redivap  11185  imdivap  11192  cjdivap  11220  maxleast  11524  lemininf  11545  ltmininf  11546  bdtrilem  11550  bdtri  11551  xrmaxaddlem  11571  xrmaxadd  11572  xrmineqinf  11580  xrltmininf  11581  xrminltinf  11583  xrminadd  11586  climuni  11604  reccn2ap  11624  isumz  11700  fsumsplitsnun  11730  geoisum1c  11831  prodfap0  11856  prod1dc  11897  fprodabs  11927  cos12dec  12079  summodnegmod  12133  dvdsmultr2  12144  mulmoddvds  12174  divalglemeuneg  12234  gcdaddm  12305  gcdass  12336  mulgcd  12337  gcddiv  12340  nnminle  12356  lcmass  12407  mulgcddvds  12416  qredeq  12418  congr  12422  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  prmexpb  12473  rpexp  12475  pythagtriplem1  12588  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem15  12601  pythagtriplem19  12605  pcdiv  12625  dvdsprmpweqle  12660  sumhashdc  12670  pcbc  12674  4sqlem12  12725  4sqlem18  12731  unennn  12768  nninfdc  12824  fvsetsid  12866  ressressg  12907  rngmulrg  12970  imasaddvallemg  13147  qusaddvallemg  13165  mgmsscl  13193  plusfvalg  13195  ress0g  13275  imasmnd2  13284  imasmnd  13285  gsumfzz  13327  grpasscan2  13396  grpidrcan  13397  grpidlcan  13398  grpinvadd  13410  grppncan  13423  dfgrp3me  13432  grpsubpropd2  13437  pwsinvg  13444  imasgrp2  13446  imasgrp  13447  mhmmnd  13452  mulgnnsubcl  13470  mulgnn0subcl  13471  mulgsubcl  13472  mulgaddcomlem  13481  mulgaddcom  13482  mulgpropdg  13500  submmulg  13502  subgcl  13520  subgsubcl  13521  subgsub  13522  subgmulg  13524  nsgconj  13542  ghmsub  13587  ghmnsgima  13604  ghmeqker  13607  f1ghm0to0  13608  ablinvadd  13646  ablpncan2  13652  subgabl  13668  rngcl  13706  imasrng  13718  srgcl  13732  ringcl  13775  crngcom  13776  ringidss  13791  ringcom  13793  mulgass2  13820  imasring  13826  opprringbg  13842  unitmulcl  13875  unitmulclb  13876  dvrcl  13897  unitdvcl  13898  dvrcan1  13902  dvrcan3  13903  rhmmul  13926  subrngmcl  13971  subrgmcl  13995  subrgdv  14000  domneq0  14034  islmod  14053  scafvalg  14069  lmodcom  14095  lmodprop2d  14110  rmodislmodlem  14112  rmodislmod  14113  lsselg  14123  lssvnegcl  14138  lspss  14161  lspun  14164  lspsnvsi  14180  lsslsp  14191  sralmod  14212  lidlnegcl  14247  rspssp  14256  rnglidlrng  14260  qus2idrng  14287  zndvds  14411  basgen  14552  2basgeng  14554  ntrss  14591  neiss  14622  opnneiss  14630  restco  14646  restabs  14647  cnprcl2k  14678  cnpf2  14679  lmconst  14688  cnpnei  14691  cnptoprest  14711  cnmpt2t  14765  psmetsym  14801  psmetge0  14803  xmetge0  14837  xmetsym  14840  blvalps  14860  blval  14861  ssblps  14897  ssbl  14898  blpnfctr  14911  xmssym  14941  bdxmet  14973  metcnp3  14983  dvfvalap  15153  dvid  15167  dvidre  15169  dvcnp2cntop  15171  elplyr  15212  ply1term  15215  plypow  15216  ptolemy  15296  rpcxpadd  15377  rpcxpsub  15380  rpmulcxp  15381  cxpmul  15384  rpcxple2  15390  rpcxplt2  15391  cxpcom  15410  rplogbval  15417  rplogbcl  15418  rplogbchbase  15422  rplogbreexp  15425  relogbexpap  15430  logbleb  15433  logblt  15434  rplogbcxp  15435  rpcxplogb  15436  relogbcxpbap  15437  sgmppw  15464  lgslem1  15477  lgsfvalg  15482  lgsval4  15497  lgsneg  15501  lgsne0  15515  lgsdinn0  15525  lgsquad  15557  funvtxvalg  15633  funiedgvalg  15634