Theorem simp3 999

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  simpl3  1002  simpr3  1005  simp3i  1008  simp3d  1011  simp13  1029  simp23  1032  simp33  1035  3anibar  1165  3ianorr  1309  stoic4a  1432  stoic4b  1433  mob2  2919  sotri2  5028  sotri3  5029  feq123  5359  resasplitss  5397  sefvex  5538  ftpg  5703  fsnunf  5719  fnfvima  5754  cocan1  5791  cocan2  5792  f1oiso2  5831  riotass  5861  moriotass  5862  ovmpox  6006  ovmpoga  6007  caovimo  6071  ofrval  6096  dfsmo2  6291  tfr1onlembfn  6348  tfrcllembfn  6361  freccllem  6406  frecfcllem  6408  frecsuclem  6410  frecrdg  6412  nnsucsssuc  6496  f1oen2g  6758  f1dom2g  6759  xpdom3m  6837  mapxpen  6851  diffifi  6897  unfidisj  6924  undifdc  6926  ssfidc  6937  sbthlemi9  6967  ctssdc  7115  endjudisj  7212  djuassen  7219  xpdjuen  7220  mulcanenq  7387  ltanqg  7402  addnnnq0  7451  nnanq0  7460  prltlu  7489  distrprg  7590  ltexprlemm  7602  recexprlem1ssl  7635  recexprlem1ssu  7636  addsrpr  7747  mulsrpr  7748  mulasssrg  7760  recexgt0sr  7775  ltpsrprg  7805  axmulass  7875  axpre-ltadd  7888  ltxrlt  8026  subadd2  8164  addsubass  8170  nppcan  8182  nppcan3  8184  subcan2  8185  subsub2  8188  subsub4  8193  pnpcan  8199  pnncan  8201  subcan  8215  subdi  8345  ltadd1  8389  leadd1  8390  leadd2  8391  ltsubadd  8392  ltsubadd2  8393  lesubadd  8394  lesubadd2  8395  ltaddsub  8396  leaddsub  8398  lesub1  8416  lesub2  8417  ltsub1  8418  ltsub2  8419  ltaddsublt  8531  gt0add  8533  reapadd1  8556  remulext1  8559  remulext2  8560  apadd2  8569  mulext2  8573  mulap0r  8575  leltap  8585  ltap  8593  apsub1  8602  divap0b  8643  divmulasscomap  8656  divcanap5  8674  dmdcanap  8682  redivclap  8691  div2negap  8695  lt2msq1  8845  ltdiv2  8847  nndivtr  8964  difgtsumgt  9325  gtndiv  9351  eluzsub  9560  nn01to3  9620  qdivcl  9646  irrmul  9650  rpgecl  9685  divge1  9726  xaddass  9872  xltadd1  9879  ubioog  9917  ubioc1  9932  lbico1  9933  iccleub  9934  lbicc2  9987  ubicc2  9988  icoshftf1o  9994  fzen  10046  elfz1b  10093  uznfz  10106  elfzo0  10185  elfzo0z  10187  ubmelfzo  10203  fzonn0p1p1  10216  ubmelm1fzo  10229  qbtwnre  10260  flqwordi  10291  flltdivnn0lt  10307  ceiqle  10316  modqval  10327  modqvalr  10328  modqcl  10329  flqpmodeq  10330  modq0  10332  mulqmod0  10333  negqmod0  10334  modqge0  10335  modqlt  10336  modqdiffl  10338  modqdifz  10339  modqmulnn  10345  modqvalp1  10346  modqabs2  10361  modqmuladdnn0  10371  qnegmod  10372  addmodid  10375  modqeqmodmin  10397  modfzo0difsn  10398  addmodlteq  10401  frec2uzf1od  10409  expnegap0  10531  expgt1  10561  exprecap  10564  expaddzaplem  10566  expaddzap  10567  expmulzap  10569  mulbinom2  10640  expnbnd  10647  fihashss  10799  fimaxq  10810  seq3coll  10825  shftfibg  10832  redivap  10886  imdivap  10893  cjdivap  10921  maxleast  11225  lemininf  11245  ltmininf  11246  bdtrilem  11250  bdtri  11251  xrmaxaddlem  11271  xrmaxadd  11272  xrmineqinf  11280  xrltmininf  11281  xrminltinf  11283  xrminadd  11286  climuni  11304  reccn2ap  11324  isumz  11400  fsumsplitsnun  11430  geoisum1c  11531  prodfap0  11556  prod1dc  11597  fprodabs  11627  cos12dec  11778  summodnegmod  11832  dvdsmultr2  11843  mulmoddvds  11872  divalglemeuneg  11931  zsupssdc  11958  gcdaddm  11988  gcdass  12019  mulgcd  12020  gcddiv  12023  nnminle  12039  lcmass  12088  mulgcddvds  12097  qredeq  12099  congr  12103  divgcdcoprmex  12105  cncongr1  12106  cncongr2  12107  prmexpb  12154  rpexp  12156  pythagtriplem1  12268  pythagtriplem6  12273  pythagtriplem7  12274  pythagtriplem12  12278  pythagtriplem13  12279  pythagtriplem15  12281  pythagtriplem19  12285  pcdiv  12305  dvdsprmpweqle  12339  sumhashdc  12348  pcbc  12352  unennn  12401  nninfdc  12457  fvsetsid  12499  ressressg  12537  rngmulrg  12599  imasaddvallemg  12742  qusaddvallemg  12759  mgmsscl  12787  plusfvalg  12789  ress0g  12852  grpasscan2  12945  grpidrcan  12946  grpidlcan  12947  grpinvadd  12959  grppncan  12972  dfgrp3me  12981  grpsubpropd2  12986  imasgrp2  12989  mhmmnd  12993  mulgnnsubcl  13009  mulgnn0subcl  13010  mulgsubcl  13011  mulgaddcomlem  13020  mulgaddcom  13021  mulgpropdg  13039  subgcl  13058  subgsubcl  13059  subgsub  13060  subgmulg  13062  nsgconj  13080  ablinvadd  13128  ablpncan2  13134  rngcl  13170  srgcl  13191  ringcl  13234  crngcom  13235  ringidss  13250  ringcom  13252  mulgass2  13273  opprringbg  13288  unitmulcl  13320  unitmulclb  13321  dvrcl  13342  unitdvcl  13343  dvrcan1  13347  dvrcan3  13348  subrgmcl  13392  subrgdv  13397  islmod  13419  scafvalg  13435  lmodcom  13461  lmodprop2d  13476  rmodislmodlem  13478  rmodislmod  13479  lsselg  13486  lssvnegcl  13501  lspss  13524  lspun  13527  lspsnvsi  13543  lsslsp  13554  sralmod  13575  lidlnegcl  13604  rspssp  13612  basgen  13768  2basgeng  13770  ntrss  13807  neiss  13838  opnneiss  13846  restco  13862  restabs  13863  cnprcl2k  13894  cnpf2  13895  lmconst  13904  cnpnei  13907  cnptoprest  13927  cnmpt2t  13981  psmetsym  14017  psmetge0  14019  xmetge0  14053  xmetsym  14056  blvalps  14076  blval  14077  ssblps  14113  ssbl  14114  blpnfctr  14127  xmssym  14157  bdxmet  14189  metcnp3  14199  dvfvalap  14338  dvid  14350  dvcnp2cntop  14351  ptolemy  14433  rpcxpadd  14514  rpcxpsub  14517  rpmulcxp  14518  cxpmul  14521  rpcxple2  14526  rpcxplt2  14527  cxpcom  14545  rplogbval  14551  rplogbcl  14552  rplogbchbase  14556  rplogbreexp  14559  relogbexpap  14564  logbleb  14567  logblt  14568  rplogbcxp  14569  rpcxplogb  14570  relogbcxpbap  14571  lgslem1  14589  lgsfvalg  14594  lgsval4  14609  lgsneg  14613  lgsne0  14627  lgsdinn0  14637