Theorem simp2 1025

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simpl2  1028  simpr2  1031  simp2i  1034  simp2d  1037  simp12  1055  simp22  1058  simp32  1061  syld3an3  1319  3ianorr  1346  intn3an2d  1394  stoic4b  1478  nlim0  4515  tfisi  4709  sotri2  5160  sotri3  5161  feq123  5500  sefvex  5691  fvmptt  5769  fnfvima  5921  cocan1  5960  cocan2  5961  ovexg  6084  ovmpox  6182  ovmpoga  6183  fvmpopr2d  6190  caovimo  6248  suppval1  6439  suppimacnvfn  6446  suppfnss  6457  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfrcllembxssdm  6587  tfrcllembfn  6588  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecrdg  6639  domssr  7017  mapxpen  7101  dif1en  7136  diffifi  7151  unsnfidcex  7180  unfidisj  7182  undifdc  7184  resfnfinfinss  7206  funrnfi  7209  fissfi  7216  sbthlemi9  7235  elfir  7260  difinfsn  7391  ctssdc  7404  djuassen  7524  xpdjuen  7525  mulcanenq  7700  ltanqg  7715  mulcanenq0ec  7760  addnnnq0  7764  distrprg  7903  aptipr  7956  addsrpr  8060  mulsrpr  8061  mulasssrg  8073  ltpsrprg  8118  axmulass  8188  axpre-ltadd  8201  subadd2  8477  nppcan  8495  nppcan3  8497  subsub2  8501  subsub4  8506  npncan3  8511  pnpcan  8512  pnncan  8514  subcan  8528  ltadd1  8703  leadd1  8704  leadd2  8705  ltsubadd  8706  ltsubadd2  8707  lesubadd  8708  lesubadd2  8709  ltaddsub  8710  leaddsub  8712  lesub1  8730  lesub2  8731  ltsub1  8732  ltsub2  8733  gt0add  8847  apreap  8861  lemul1  8867  reapmul1lem  8868  reapmul1  8869  reapadd1  8870  remulext1  8873  remulext2  8874  apadd2  8883  mulext2  8887  mulap0r  8889  leltap  8899  ltap  8907  apsub1  8916  recexaplem2  8926  mulcanap  8939  mulcanap2  8940  divvalap  8948  divmulap  8949  divcanap1  8955  diveqap0  8956  divap0b  8957  divrecap  8962  divassap  8964  div23ap  8965  divdirap  8971  divcanap3  8972  div11ap  8974  diveqap1  8979  divmuldivap  8986  divcanap5  8988  redivclap  9005  div2negap  9009  apmul1  9062  apmul2  9063  div2subap  9111  ltdiv1  9142  ledivmul  9151  lemuldiv  9155  lt2msq1  9159  ltdiv23  9166  squeeze0  9178  ofnegsub  9236  zaddcllemneg  9616  eluzsub  9884  nn01to3  9949  rpgecl  10015  addlelt  10101  xleadd1  10208  xltadd1  10209  lbioog  10246  ubioc1  10262  ubicc2  10318  icoshftf1o  10324  fzen  10377  nelfzo  10486  ubmelfzo  10545  ssfzo12  10569  ubmelm1fzo  10571  fzosplitprm1  10580  zsupssdc  10598  rebtwn2zlemshrink  10613  qbtwnre  10616  icogelb  10625  flqwordi  10648  flqword2  10649  flltdivnn0lt  10664  modqcl  10688  mulqmod0  10692  modqmulnn  10704  modqabs2  10720  modqmuladdnn0  10730  qnegmod  10731  addmodid  10734  modqm1p1mod0  10737  modifeq2int  10748  modqdi  10754  modqeqmodmin  10756  modfzo0difsn  10757  frec2uzf1od  10768  exp3val  10903  expnegap0  10909  expgt1  10939  exprecap  10942  expmulzap  10947  leexp2a  10954  expubnd  10958  mulbinom2  11018  bernneq2  11023  expnbnd  11025  fihashss  11181  fihashssdif  11183  fimaxq  11194  ccatval2  11286  ccatass  11296  ccatw2s1leng  11326  ccat2s1fvwd  11335  swrdval  11340  swrdnd  11351  pfxfv  11376  pfxpfx  11400  ccats1pfxeq  11406  ccats1pfxeqrex  11407  s3cl  11478  s3fv0g  11483  s3fv1g  11484  s3fv2g  11485  shftuz  11502  shftfibg  11505  cjdivap  11594  resqrtcl  11714  absdivap  11755  abssubne0  11776  maxleast  11898  lemininf  11919  ltmininf  11920  xrmaxltsup  11943  xrmaxaddlem  11945  xrmaxadd  11946  xrmineqinf  11954  xrltmininf  11955  xrminltinf  11957  xrminadd  11960  climuni  11978  reccn2ap  11998  isumz  12075  geoisum1c  12206  prod1dc  12272  efltim  12384  dvdsval2  12476  dvdscmulr  12506  dvdsmulcr  12507  modmulconst  12509  dvdsadd2b  12526  dvdsexp  12547  mulmoddvds  12549  divalglemeuneg  12609  gcdaddm  12680  dvdsgcdb  12709  mulgcd  12712  gcddiv  12715  uzwodc  12733  lcmdvdsb  12781  mulgcddvds  12791  qredeq  12793  divgcdcoprm0  12798  cncongr1  12800  euclemma  12843  rpexp  12850  rpexp12i  12852  fermltl  12931  prmdiv  12932  odzcllem  12940  odzdvds  12943  odzphi  12944  vfermltl  12949  coprimeprodsq  12955  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem13  12974  pceu  12993  pcdvdsb  13018  pcgcd1  13026  dvdsprmpweq  13033  sumhashdc  13045  ctinf  13181  fvsetsid  13246  ressressg  13288  ressabsg  13289  rngplusgg  13350  imasaddvallemg  13528  qusaddvallemg  13546  plusfvalg  13576  mgmb1mgm1  13581  issubmnd  13655  ress0g  13656  imasmnd2  13665  imasmnd  13666  gsumfzz  13708  grpasscan2  13777  grpidrcan  13778  grpidlcan  13779  grpinvadd  13791  grpsubeq0  13799  grppncan  13804  dfgrp3mlem  13811  dfgrp3me  13813  grpsubpropd2  13818  pwsinvg  13825  imasgrp2  13827  imasgrp  13828  mhmmnd  13833  mulgnn0p1  13850  mulgnnsubcl  13851  mulgnn0subcl  13852  mulgsubcl  13853  mulgneg  13857  mulgaddcom  13863  mulginvcom  13864  submmulg  13883  subgcl  13901  subgsubcl  13902  subgsub  13903  subgmulg  13905  nsgconj  13923  nsgid  13932  quseccl0g  13948  ghmmulg  13973  ghmeqker  13988  f1ghm0to0  13989  kerf1ghm  13991  ablinvadd  14027  ablsub4  14030  ablpncan2  14033  subgabl  14049  gsumfzconst  14058  rngcl  14088  imasrng  14100  srgcl  14114  ringcl  14157  crngcom  14158  ringidss  14173  ringcom  14175  imasring  14208  opprringbg  14224  unitmulcl  14258  unitmulclb  14259  dvrcl  14280  unitdvcl  14281  dvrcan1  14285  dvrcan3  14286  rhmmul  14309  subrngrng  14347  subrngmcl  14354  subrgmcl  14378  subrgdv  14383  rrgeq0  14410  domneq0  14418  islmod  14439  scafvalg  14455  lmodcom  14481  rmodislmodlem  14498  rmodislmod  14499  lssclg  14512  lssvnegcl  14524  lssintclm  14532  lspss  14547  lspun  14550  lspsnvsi  14566  rspssp  14642  rnglidlmmgm  14644  rnglidlmsgrp  14645  rnglidlrng  14646  zndvds  14797  psrbaglecl  14824  psrbagcon  14826  2basgeng  14947  iuncld  14980  ntrss  14984  restco  15039  restabs  15040  cnprcl2k  15071  lmconst  15081  cnrest2  15101  cnmpt2t  15158  psmetsym  15194  psmetge0  15196  xmetge0  15230  xmetsym  15233  blvalps  15253  blval  15254  xblcntrps  15278  xblcntr  15279  xmssym  15334  blsscls2  15358  bdxmet  15366  txmetcnp  15383  dvfvalap  15546  dvid  15560  dvidre  15562  dvcnp2cntop  15564  elplyr  15605  rpcxpadd  15770  rpcxpsub  15773  rpmulcxp  15774  rpdivcxp  15776  cxpmul  15777  rpcxple2  15783  rpcxplt2  15784  rplogbval  15810  rplogbcl  15811  rplogbreexp  15818  relogbexpap  15823  logbleb  15826  logblt  15827  rplogbcxp  15828  rpcxplogb  15829  relogbcxpbap  15830  sgmppw  15860  lgsneg1  15898  lgsmod  15899  lgsne0  15911  lgssq  15913  lgsdirnn0  15920  lgsdinn0  15921  lgsquad  15953  funvtxvalg  16031  funiedgvalg  16032  lpvtx  16074  ausgrumgrien  16165  ausgrusgrien  16166  uhgrissubgr  16256  egrsubgr  16258  subumgredg2en  16266  subusgr  16270  wlkl1loop  16353  clwwlknonex2  16434  eulerpathprum  16475  eulerpathum  16476  findset  16715  repiecele0  16810  repiecege0  16811  gfsumsn  16867