Theorem simp2 1029

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp2	|- ( ( ph /\ ps /\ ch ) -> ps )

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 1025	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simprd 114	1 |- ( ( ph /\ ps /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ w3a 1009

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

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  simpl2  1032  simpr2  1035  simp2i  1038  simp2d  1041  simp12  1059  simp22  1062  simp32  1065  syld3an3  1323  3ianorr  1350  intn3an2d  1398  stoic4b  1482  nlim0  4534  tfisi  4729  sotri2  5180  sotri3  5181  feq123  5520  sefvex  5711  fvmptt  5791  fnfvima  5943  cocan1  5983  cocan2  5984  ovexg  6109  ovmpox  6207  ovmpoga  6208  fvmpopr2d  6215  caovimo  6273  suppval1  6469  suppimacnvfn  6476  suppfnss  6487  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfrcllembxssdm  6617  tfrcllembfn  6618  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecrdg  6669  domssr  7054  mapxpen  7138  dif1en  7173  diffifi  7188  unsnfidcex  7217  unfidisj  7219  undifdc  7221  resfnfinfinss  7243  funrnfi  7246  fissfi  7253  sbthlemi9  7272  elfir  7297  difinfsn  7430  ctssdc  7443  djuassen  7563  xpdjuen  7564  mulcanenq  7742  ltanqg  7757  mulcanenq0ec  7802  addnnnq0  7806  distrprg  7945  aptipr  7998  addsrpr  8102  mulsrpr  8103  mulasssrg  8115  ltpsrprg  8160  axmulass  8230  axpre-ltadd  8243  subadd2  8520  nppcan  8538  nppcan3  8540  subsub2  8544  subsub4  8549  npncan3  8554  pnpcan  8555  pnncan  8557  subcan  8571  ltadd1  8747  leadd1  8748  leadd2  8749  ltsubadd  8750  ltsubadd2  8751  lesubadd  8752  lesubadd2  8753  ltaddsub  8754  leaddsub  8756  lesub1  8774  lesub2  8775  ltsub1  8776  ltsub2  8777  gt0add  8891  apreap  8905  lemul1  8911  reapmul1lem  8912  reapmul1  8913  reapadd1  8914  remulext1  8917  remulext2  8918  apadd2  8927  mulext2  8931  mulap0r  8933  leltap  8943  ltap  8951  apsub1  8960  recexaplem2  8970  mulcanap  8983  mulcanap2  8984  divvalap  8994  divmulap  8995  divcanap1  9001  diveqap0  9002  divap0b  9003  divrecap  9008  divassap  9010  div23ap  9011  divdirap  9017  divcanap3  9018  div11ap  9020  diveqap1  9025  divmuldivap  9032  divcanap5  9034  redivclap  9051  div2negap  9055  apmul1  9108  apmul2  9109  div2subap  9157  ltdiv1  9188  ledivmul  9197  lemuldiv  9201  lt2msq1  9205  ltdiv23  9212  squeeze0  9224  ofnegsub  9282  zaddcllemneg  9662  zfidc  9702  eluzsub  9931  nn01to3  9996  rpgecl  10062  addlelt  10148  xleadd1  10256  xltadd1  10257  lbioog  10294  ubioc1  10310  ubicc2  10366  icoshftf1o  10372  fzen  10426  nelfzo  10537  ubmelfzo  10596  ssfzo12  10620  ubmelm1fzo  10622  fzosplitprm1  10631  zsupssdc  10651  rebtwn2zlemshrink  10666  qbtwnre  10669  icogelb  10678  flqwordi  10701  flqword2  10702  flltdivnn0lt  10717  modqcl  10741  mulqmod0  10745  modqmulnn  10757  modqabs2  10773  modqmuladdnn0  10783  qnegmod  10784  addmodid  10787  modqm1p1mod0  10790  modifeq2int  10801  modqdi  10807  modqeqmodmin  10809  modfzo0difsn  10810  frec2uzf1od  10821  exp3val  10956  expnegap0  10962  expgt1  10992  exprecap  10995  expmulzap  11000  leexp2a  11007  expubnd  11011  mulbinom2  11071  bernneq2  11077  expnbnd  11079  fihashss  11235  fihashssdif  11237  fimaxq  11248  ccatval2  11344  ccatass  11354  ccatw2s1leng  11384  ccat2s1fvwd  11393  swrdval  11398  swrdnd  11409  pfxfv  11434  pfxpfx  11458  ccats1pfxeq  11464  ccats1pfxeqrex  11465  s3cl  11536  s3fv0g  11541  s3fv1g  11542  s3fv2g  11543  shftuz  11560  shftfibg  11563  cjdivap  11653  resqrtcl  11773  absdivap  11814  abssubne0  11835  maxleast  11957  lemininf  11978  ltmininf  11979  xrmaxltsup  12002  xrmaxaddlem  12004  xrmaxadd  12005  xrmineqinf  12013  xrltmininf  12014  xrminltinf  12016  xrminadd  12019  climuni  12037  reccn2ap  12057  isumz  12134  geoisum1c  12265  prod1dc  12331  efltim  12443  dvdsval2  12535  dvdscmulr  12565  dvdsmulcr  12566  modmulconst  12568  dvdsadd2b  12585  dvdsexp  12606  mulmoddvds  12608  divalglemeuneg  12668  gcdaddm  12739  dvdsgcdb  12768  mulgcd  12771  gcddiv  12774  uzwodc  12792  lcmdvdsb  12840  mulgcddvds  12850  qredeq  12852  divgcdcoprm0  12857  cncongr1  12859  euclemma  12902  rpexp  12909  rpexp12i  12911  fermltl  12990  prmdiv  12991  odzcllem  12999  odzdvds  13002  odzphi  13003  vfermltl  13008  coprimeprodsq  13014  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem13  13033  pceu  13052  pcdvdsb  13077  pcgcd1  13085  dvdsprmpweq  13092  sumhashdc  13104  ctinf  13299  fvsetsid  13364  ressressg  13406  ressabsg  13407  rngplusgg  13468  imasaddvallemg  13613  qusaddvallemg  13631  plusfvalg  13660  mgmb1mgm1  13665  issubmnd  13732  ress0g  13733  imasmnd2  13736  imasmnd  13737  grpasscan2  13846  grpidrcan  13847  grpidlcan  13848  grpinvadd  13860  grpsubeq0  13868  grppncan  13873  dfgrp3mlem  13880  dfgrp3me  13882  grpsubpropd2  13887  imasgrp2  13890  imasgrp  13891  mhmmnd  13896  mulgnn0p1  13913  mulgnnsubcl  13914  mulgnn0subcl  13915  mulgsubcl  13916  mulgneg  13920  mulgaddcom  13926  mulginvcom  13927  submmulg  13946  subgcl  13964  subgsubcl  13965  subgsub  13966  subgmulg  13968  nsgconj  13986  nsgid  13995  quseccl0g  14011  ghmmulg  14036  ghmeqker  14051  f1ghm0to0  14052  kerf1ghm  14054  ablinvadd  14091  ablsub4  14094  ablpncan2  14097  subgabl  14113  gzsumconst  14120  gsumsncmn  14133  gsumconstcmn  14143  pwsinvg  14192  rngcl  14218  imasrng  14230  srgcl  14248  ringcl  14291  crngcom  14292  ringidss  14307  ringcom  14309  imasring  14342  opprringbg  14358  unitmulcl  14393  unitmulclb  14394  dvrcl  14415  unitdvcl  14416  dvrcan1  14420  dvrcan3  14421  rhmmul  14444  subrngrng  14483  subrngmcl  14490  subrgmcl  14514  subrgdv  14519  rrgeq0  14546  domneq0  14554  islmod  14600  scafvalg  14616  lmodcom  14642  rmodislmodlem  14659  rmodislmod  14660  lssclg  14673  lssvnegcl  14685  lssintclm  14693  lspss  14708  lspun  14711  lspsnvsi  14727  rspssp  14803  rnglidlmmgm  14805  rnglidlmsgrp  14806  rnglidlrng  14807  zndvds  14956  psrbaglecl  14983  psrbagcon  14985  2basgeng  15106  iuncld  15139  ntrss  15143  restco  15198  restabs  15199  cnprcl2k  15230  lmconst  15240  cnrest2  15260  cnmpt2t  15317  psmetsym  15353  psmetge0  15355  xmetge0  15389  xmetsym  15392  blvalps  15412  blval  15413  xblcntrps  15437  xblcntr  15438  xmssym  15493  blsscls2  15517  bdxmet  15525  txmetcnp  15542  dvfvalap  15705  dvid  15719  dvidre  15721  dvcnp2cntop  15723  elplyr  15764  logfac  15918  rpcxpadd  15930  rpcxpsub  15933  rpmulcxp  15934  rpdivcxp  15936  cxpmul  15937  rpcxple2  15943  rpcxplt2  15944  rplogbval  15970  rplogbcl  15971  rplogbreexp  15978  relogbexpap  15983  logbleb  15986  logblt  15987  rplogbcxp  15988  rpcxplogb  15989  relogbcxpbap  15990  sgmppw  16020  lgsneg1  16058  lgsmod  16059  lgsne0  16071  lgssq  16073  lgsdirnn0  16080  lgsdinn0  16081  lgsquad  16113  funvtxvalg  16191  funiedgvalg  16192  lpvtx  16234  ausgrumgrien  16325  ausgrusgrien  16326  uhgrissubgr  16416  egrsubgr  16418  subumgredg2en  16426  subusgr  16430  wlkl1loop  16513  clwwlknonex2  16594  eulerpathprum  16635  eulerpathum  16636  findset  16885  repiecele0  16980  repiecege0  16981