Theorem simp3 989

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

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpl3  992  simpr3  995  simp3i  998  simp3d  1001  simp13  1019  simp23  1022  simp33  1025  3anibar  1155  3ianorr  1299  stoic4a  1420  stoic4b  1421  mob2  2905  sotri2  5000  sotri3  5001  feq123  5328  resasplitss  5366  sefvex  5506  ftpg  5668  fsnunf  5684  fnfvima  5718  cocan1  5754  cocan2  5755  f1oiso2  5794  riotass  5824  moriotass  5825  ovmpox  5966  ovmpoga  5967  caovimo  6031  ofrval  6059  dfsmo2  6251  tfr1onlembfn  6308  tfrcllembfn  6321  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecrdg  6372  nnsucsssuc  6456  f1oen2g  6717  f1dom2g  6718  xpdom3m  6796  mapxpen  6810  diffifi  6856  unfidisj  6883  undifdc  6885  ssfidc  6896  sbthlemi9  6926  ctssdc  7074  endjudisj  7162  djuassen  7169  xpdjuen  7170  mulcanenq  7322  ltanqg  7337  addnnnq0  7386  nnanq0  7395  prltlu  7424  distrprg  7525  ltexprlemm  7537  recexprlem1ssl  7570  recexprlem1ssu  7571  addsrpr  7682  mulsrpr  7683  mulasssrg  7695  recexgt0sr  7710  ltpsrprg  7740  axmulass  7810  axpre-ltadd  7823  ltxrlt  7960  subadd2  8098  addsubass  8104  nppcan  8116  nppcan3  8118  subcan2  8119  subsub2  8122  subsub4  8127  pnpcan  8133  pnncan  8135  subcan  8149  subdi  8279  ltadd1  8323  leadd1  8324  leadd2  8325  ltsubadd  8326  ltsubadd2  8327  lesubadd  8328  lesubadd2  8329  ltaddsub  8330  leaddsub  8332  lesub1  8350  lesub2  8351  ltsub1  8352  ltsub2  8353  ltaddsublt  8465  gt0add  8467  reapadd1  8490  remulext1  8493  remulext2  8494  apadd2  8503  mulext2  8507  mulap0r  8509  leltap  8519  ltap  8527  apsub1  8536  divap0b  8575  divmulasscomap  8588  divcanap5  8606  dmdcanap  8614  redivclap  8623  div2negap  8627  lt2msq1  8776  ltdiv2  8778  nndivtr  8895  difgtsumgt  9256  gtndiv  9282  eluzsub  9491  nn01to3  9551  qdivcl  9577  irrmul  9581  rpgecl  9614  divge1  9655  xaddass  9801  xltadd1  9808  ubioog  9846  ubioc1  9861  lbico1  9862  iccleub  9863  lbicc2  9916  ubicc2  9917  icoshftf1o  9923  fzen  9974  elfz1b  10021  uznfz  10034  elfzo0  10113  elfzo0z  10115  ubmelfzo  10131  fzonn0p1p1  10144  ubmelm1fzo  10157  qbtwnre  10188  flqwordi  10219  flltdivnn0lt  10235  ceiqle  10244  modqval  10255  modqvalr  10256  modqcl  10257  flqpmodeq  10258  modq0  10260  mulqmod0  10261  negqmod0  10262  modqge0  10263  modqlt  10264  modqdiffl  10266  modqdifz  10267  modqmulnn  10273  modqvalp1  10274  modqabs2  10289  modqmuladdnn0  10299  qnegmod  10300  addmodid  10303  modqeqmodmin  10325  modfzo0difsn  10326  addmodlteq  10329  frec2uzf1od  10337  expnegap0  10459  expgt1  10489  exprecap  10492  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  mulbinom2  10567  expnbnd  10574  fihashss  10725  fimaxq  10736  seq3coll  10751  shftfibg  10758  redivap  10812  imdivap  10819  cjdivap  10847  maxleast  11151  lemininf  11171  ltmininf  11172  bdtrilem  11176  bdtri  11177  xrmaxaddlem  11197  xrmaxadd  11198  xrmineqinf  11206  xrltmininf  11207  xrminltinf  11209  xrminadd  11212  climuni  11230  reccn2ap  11250  isumz  11326  fsumsplitsnun  11356  geoisum1c  11457  prodfap0  11482  prod1dc  11523  fprodabs  11553  cos12dec  11704  summodnegmod  11758  dvdsmultr2  11769  mulmoddvds  11797  divalglemeuneg  11856  zsupssdc  11883  gcdaddm  11913  gcdass  11944  mulgcd  11945  gcddiv  11948  nnminle  11964  lcmass  12013  mulgcddvds  12022  qredeq  12024  congr  12028  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  prmexpb  12079  rpexp  12081  pythagtriplem1  12193  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem13  12204  pythagtriplem15  12206  pythagtriplem19  12210  pcdiv  12230  dvdsprmpweqle  12264  sumhashdc  12273  pcbc  12277  unennn  12326  nninfdc  12382  fvsetsid  12424  ressid2  12449  ressval2  12450  rngmulrg  12508  basgen  12680  2basgeng  12682  ntrss  12719  neiss  12750  opnneiss  12758  restco  12774  restabs  12775  cnprcl2k  12806  cnpf2  12807  lmconst  12816  cnpnei  12819  cnptoprest  12839  cnmpt2t  12893  psmetsym  12929  psmetge0  12931  xmetge0  12965  xmetsym  12968  blvalps  12988  blval  12989  ssblps  13025  ssbl  13026  blpnfctr  13039  xmssym  13069  bdxmet  13101  metcnp3  13111  dvfvalap  13250  dvid  13262  dvcnp2cntop  13263  ptolemy  13345  rpcxpadd  13426  rpcxpsub  13429  rpmulcxp  13430  cxpmul  13433  rpcxple2  13438  rpcxplt2  13439  cxpcom  13457  rplogbval  13463  rplogbcl  13464  rplogbchbase  13468  rplogbreexp  13471  relogbexpap  13476  logbleb  13479  logblt  13480  rplogbcxp  13481  rpcxplogb  13482  relogbcxpbap  13483  lgslem1  13501  lgsfvalg  13506  lgsval4  13521  lgsneg  13525  lgsne0  13539  lgsdinn0  13549