Theorem simp3 983

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

Syntax hints:   -> wi 4   /\ w3a 962

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 964

This theorem is referenced by:  simpl3  986  simpr3  989  simp3i  992  simp3d  995  simp13  1013  simp23  1016  simp33  1019  3anibar  1149  3ianorr  1287  stoic4a  1408  stoic4b  1409  mob2  2859  sotri2  4931  sotri3  4932  feq123  5259  resasplitss  5297  sefvex  5435  ftpg  5597  fsnunf  5613  fnfvima  5645  cocan1  5681  cocan2  5682  f1oiso2  5721  riotass  5750  moriotass  5751  ovmpox  5892  ovmpoga  5893  caovimo  5957  ofrval  5985  dfsmo2  6177  tfr1onlembfn  6234  tfrcllembfn  6247  freccllem  6292  frecfcllem  6294  frecsuclem  6296  frecrdg  6298  nnsucsssuc  6381  f1oen2g  6642  f1dom2g  6643  xpdom3m  6721  mapxpen  6735  diffifi  6781  unfidisj  6803  undifdc  6805  ssfidc  6816  sbthlemi9  6846  ctssdc  6991  endjudisj  7059  djuassen  7066  xpdjuen  7067  mulcanenq  7186  ltanqg  7201  addnnnq0  7250  nnanq0  7259  prltlu  7288  distrprg  7389  ltexprlemm  7401  recexprlem1ssl  7434  recexprlem1ssu  7435  addsrpr  7546  mulsrpr  7547  mulasssrg  7559  recexgt0sr  7574  ltpsrprg  7604  axmulass  7674  axpre-ltadd  7687  ltxrlt  7823  subadd2  7959  addsubass  7965  nppcan  7977  nppcan3  7979  subcan2  7980  subsub2  7983  subsub4  7988  pnpcan  7994  pnncan  7996  subcan  8010  subdi  8140  ltadd1  8184  leadd1  8185  leadd2  8186  ltsubadd  8187  ltsubadd2  8188  lesubadd  8189  lesubadd2  8190  ltaddsub  8191  leaddsub  8193  lesub1  8211  lesub2  8212  ltsub1  8213  ltsub2  8214  ltaddsublt  8326  gt0add  8328  reapadd1  8351  remulext1  8354  remulext2  8355  apadd2  8364  mulext2  8368  mulap0r  8370  leltap  8380  ltap  8388  apsub1  8397  divap0b  8436  divmulasscomap  8449  divcanap5  8467  dmdcanap  8475  redivclap  8484  div2negap  8488  lt2msq1  8636  ltdiv2  8638  nndivtr  8755  gtndiv  9139  eluzsub  9348  nn01to3  9402  qdivcl  9428  irrmul  9432  rpgecl  9463  divge1  9503  xaddass  9645  xltadd1  9652  ubioog  9690  ubioc1  9705  lbico1  9706  iccleub  9707  lbicc2  9760  ubicc2  9761  icoshftf1o  9767  fzen  9816  elfz1b  9863  uznfz  9876  elfzo0  9952  elfzo0z  9954  ubmelfzo  9970  fzonn0p1p1  9983  ubmelm1fzo  9996  qbtwnre  10027  flqwordi  10054  flltdivnn0lt  10070  ceiqle  10079  modqval  10090  modqvalr  10091  modqcl  10092  flqpmodeq  10093  modq0  10095  mulqmod0  10096  negqmod0  10097  modqge0  10098  modqlt  10099  modqdiffl  10101  modqdifz  10102  modqmulnn  10108  modqvalp1  10109  modqabs2  10124  modqmuladdnn0  10134  qnegmod  10135  addmodid  10138  modqeqmodmin  10160  modfzo0difsn  10161  addmodlteq  10164  frec2uzf1od  10172  expnegap0  10294  expgt1  10324  exprecap  10327  expaddzaplem  10329  expaddzap  10330  expmulzap  10332  mulbinom2  10401  expnbnd  10408  fihashss  10555  fimaxq  10566  seq3coll  10578  shftfibg  10585  redivap  10639  imdivap  10646  cjdivap  10674  maxleast  10978  lemininf  10998  ltmininf  10999  bdtrilem  11003  bdtri  11004  xrmaxaddlem  11022  xrmaxadd  11023  xrmineqinf  11031  xrltmininf  11032  xrminltinf  11034  xrminadd  11037  climuni  11055  reccn2ap  11075  isumz  11151  fsumsplitsnun  11181  geoisum1c  11282  prodfap0  11307  cos12dec  11463  summodnegmod  11513  dvdsmultr2  11522  mulmoddvds  11550  divalglemeuneg  11609  gcdaddm  11661  gcdass  11692  mulgcd  11693  gcddiv  11696  lcmass  11755  mulgcddvds  11764  qredeq  11766  congr  11770  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  prmexpb  11818  rpexp  11820  unennn  11899  fvsetsid  11982  ressid2  12007  ressval2  12008  rngmulrg  12066  basgen  12238  2basgeng  12240  ntrss  12277  neiss  12308  opnneiss  12316  restco  12332  restabs  12333  cnprcl2k  12364  cnpf2  12365  lmconst  12374  cnpnei  12377  cnptoprest  12397  cnmpt2t  12451  psmetsym  12487  psmetge0  12489  xmetge0  12523  xmetsym  12526  blvalps  12546  blval  12547  ssblps  12583  ssbl  12584  blpnfctr  12597  xmssym  12627  bdxmet  12659  metcnp3  12669  dvfvalap  12808  dvid  12820  dvcnp2cntop  12821  ptolemy  12894