Theorem simp3 984

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

Syntax hints:   -> wi 4   /\ w3a 963

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 965

This theorem is referenced by:  simpl3  987  simpr3  990  simp3i  993  simp3d  996  simp13  1014  simp23  1017  simp33  1020  3anibar  1150  3ianorr  1291  stoic4a  1412  stoic4b  1413  mob2  2892  sotri2  4986  sotri3  4987  feq123  5314  resasplitss  5352  sefvex  5492  ftpg  5654  fsnunf  5670  fnfvima  5704  cocan1  5740  cocan2  5741  f1oiso2  5780  riotass  5810  moriotass  5811  ovmpox  5952  ovmpoga  5953  caovimo  6017  ofrval  6045  dfsmo2  6237  tfr1onlembfn  6294  tfrcllembfn  6307  freccllem  6352  frecfcllem  6354  frecsuclem  6356  frecrdg  6358  nnsucsssuc  6442  f1oen2g  6703  f1dom2g  6704  xpdom3m  6782  mapxpen  6796  diffifi  6842  unfidisj  6869  undifdc  6871  ssfidc  6882  sbthlemi9  6912  ctssdc  7060  endjudisj  7148  djuassen  7155  xpdjuen  7156  mulcanenq  7308  ltanqg  7323  addnnnq0  7372  nnanq0  7381  prltlu  7410  distrprg  7511  ltexprlemm  7523  recexprlem1ssl  7556  recexprlem1ssu  7557  addsrpr  7668  mulsrpr  7669  mulasssrg  7681  recexgt0sr  7696  ltpsrprg  7726  axmulass  7796  axpre-ltadd  7809  ltxrlt  7946  subadd2  8084  addsubass  8090  nppcan  8102  nppcan3  8104  subcan2  8105  subsub2  8108  subsub4  8113  pnpcan  8119  pnncan  8121  subcan  8135  subdi  8265  ltadd1  8309  leadd1  8310  leadd2  8311  ltsubadd  8312  ltsubadd2  8313  lesubadd  8314  lesubadd2  8315  ltaddsub  8316  leaddsub  8318  lesub1  8336  lesub2  8337  ltsub1  8338  ltsub2  8339  ltaddsublt  8451  gt0add  8453  reapadd1  8476  remulext1  8479  remulext2  8480  apadd2  8489  mulext2  8493  mulap0r  8495  leltap  8505  ltap  8513  apsub1  8522  divap0b  8561  divmulasscomap  8574  divcanap5  8592  dmdcanap  8600  redivclap  8609  div2negap  8613  lt2msq1  8762  ltdiv2  8764  nndivtr  8881  gtndiv  9265  eluzsub  9474  nn01to3  9533  qdivcl  9559  irrmul  9563  rpgecl  9596  divge1  9637  xaddass  9780  xltadd1  9787  ubioog  9825  ubioc1  9840  lbico1  9841  iccleub  9842  lbicc2  9895  ubicc2  9896  icoshftf1o  9902  fzen  9952  elfz1b  9999  uznfz  10012  elfzo0  10091  elfzo0z  10093  ubmelfzo  10109  fzonn0p1p1  10122  ubmelm1fzo  10135  qbtwnre  10166  flqwordi  10197  flltdivnn0lt  10213  ceiqle  10222  modqval  10233  modqvalr  10234  modqcl  10235  flqpmodeq  10236  modq0  10238  mulqmod0  10239  negqmod0  10240  modqge0  10241  modqlt  10242  modqdiffl  10244  modqdifz  10245  modqmulnn  10251  modqvalp1  10252  modqabs2  10267  modqmuladdnn0  10277  qnegmod  10278  addmodid  10281  modqeqmodmin  10303  modfzo0difsn  10304  addmodlteq  10307  frec2uzf1od  10315  expnegap0  10437  expgt1  10467  exprecap  10470  expaddzaplem  10472  expaddzap  10473  expmulzap  10475  mulbinom2  10544  expnbnd  10551  fihashss  10702  fimaxq  10713  seq3coll  10725  shftfibg  10732  redivap  10786  imdivap  10793  cjdivap  10821  maxleast  11125  lemininf  11145  ltmininf  11146  bdtrilem  11150  bdtri  11151  xrmaxaddlem  11169  xrmaxadd  11170  xrmineqinf  11178  xrltmininf  11179  xrminltinf  11181  xrminadd  11184  climuni  11202  reccn2ap  11222  isumz  11298  fsumsplitsnun  11328  geoisum1c  11429  prodfap0  11454  prod1dc  11495  fprodabs  11525  cos12dec  11676  summodnegmod  11730  dvdsmultr2  11740  mulmoddvds  11768  divalglemeuneg  11827  zsupssdc  11854  gcdaddm  11884  gcdass  11915  mulgcd  11916  gcddiv  11919  lcmass  11978  mulgcddvds  11987  qredeq  11989  congr  11993  divgcdcoprmex  11995  cncongr1  11996  cncongr2  11997  prmexpb  12042  rpexp  12044  pythagtriplem1  12156  pythagtriplem6  12161  pythagtriplem7  12162  pythagtriplem12  12166  pythagtriplem13  12167  pythagtriplem15  12169  pythagtriplem19  12173  pcdiv  12193  unennn  12222  nnminle  12274  nninfdc  12280  fvsetsid  12320  ressid2  12345  ressval2  12346  rngmulrg  12404  basgen  12576  2basgeng  12578  ntrss  12615  neiss  12646  opnneiss  12654  restco  12670  restabs  12671  cnprcl2k  12702  cnpf2  12703  lmconst  12712  cnpnei  12715  cnptoprest  12735  cnmpt2t  12789  psmetsym  12825  psmetge0  12827  xmetge0  12861  xmetsym  12864  blvalps  12884  blval  12885  ssblps  12921  ssbl  12922  blpnfctr  12935  xmssym  12965  bdxmet  12997  metcnp3  13007  dvfvalap  13146  dvid  13158  dvcnp2cntop  13159  ptolemy  13241  rpcxpadd  13322  rpcxpsub  13325  rpmulcxp  13326  cxpmul  13329  rpcxple2  13334  rpcxplt2  13335  cxpcom  13353  rplogbval  13359  rplogbcl  13360  rplogbchbase  13364  rplogbreexp  13367  relogbexpap  13372  logbleb  13375  logblt  13376  rplogbcxp  13377  rpcxplogb  13378  relogbcxpbap  13379