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  4520  tfisi  4714  sotri2  5165  sotri3  5166  feq123  5505  sefvex  5696  fvmptt  5774  fnfvima  5926  cocan1  5966  cocan2  5967  ovexg  6092  ovmpox  6190  ovmpoga  6191  fvmpopr2d  6198  caovimo  6256  suppval1  6452  suppimacnvfn  6459  suppfnss  6470  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfrcllembxssdm  6600  tfrcllembfn  6601  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecrdg  6652  domssr  7030  mapxpen  7114  dif1en  7149  diffifi  7164  unsnfidcex  7193  unfidisj  7195  undifdc  7197  resfnfinfinss  7219  funrnfi  7222  fissfi  7229  sbthlemi9  7248  elfir  7273  difinfsn  7404  ctssdc  7417  djuassen  7537  xpdjuen  7538  mulcanenq  7716  ltanqg  7731  mulcanenq0ec  7776  addnnnq0  7780  distrprg  7919  aptipr  7972  addsrpr  8076  mulsrpr  8077  mulasssrg  8089  ltpsrprg  8134  axmulass  8204  axpre-ltadd  8217  subadd2  8493  nppcan  8511  nppcan3  8513  subsub2  8517  subsub4  8522  npncan3  8527  pnpcan  8528  pnncan  8530  subcan  8544  ltadd1  8720  leadd1  8721  leadd2  8722  ltsubadd  8723  ltsubadd2  8724  lesubadd  8725  lesubadd2  8726  ltaddsub  8727  leaddsub  8729  lesub1  8747  lesub2  8748  ltsub1  8749  ltsub2  8750  gt0add  8864  apreap  8878  lemul1  8884  reapmul1lem  8885  reapmul1  8886  reapadd1  8887  remulext1  8890  remulext2  8891  apadd2  8900  mulext2  8904  mulap0r  8906  leltap  8916  ltap  8924  apsub1  8933  recexaplem2  8943  mulcanap  8956  mulcanap2  8957  divvalap  8965  divmulap  8966  divcanap1  8972  diveqap0  8973  divap0b  8974  divrecap  8979  divassap  8981  div23ap  8982  divdirap  8988  divcanap3  8989  div11ap  8991  diveqap1  8996  divmuldivap  9003  divcanap5  9005  redivclap  9022  div2negap  9026  apmul1  9079  apmul2  9080  div2subap  9128  ltdiv1  9159  ledivmul  9168  lemuldiv  9172  lt2msq1  9176  ltdiv23  9183  squeeze0  9195  ofnegsub  9253  zaddcllemneg  9633  zfidc  9673  eluzsub  9902  nn01to3  9967  rpgecl  10033  addlelt  10119  xleadd1  10227  xltadd1  10228  lbioog  10265  ubioc1  10281  ubicc2  10337  icoshftf1o  10343  fzen  10397  nelfzo  10508  ubmelfzo  10567  ssfzo12  10591  ubmelm1fzo  10593  fzosplitprm1  10602  zsupssdc  10622  rebtwn2zlemshrink  10637  qbtwnre  10640  icogelb  10649  flqwordi  10672  flqword2  10673  flltdivnn0lt  10688  modqcl  10712  mulqmod0  10716  modqmulnn  10728  modqabs2  10744  modqmuladdnn0  10754  qnegmod  10755  addmodid  10758  modqm1p1mod0  10761  modifeq2int  10772  modqdi  10778  modqeqmodmin  10780  modfzo0difsn  10781  frec2uzf1od  10792  exp3val  10927  expnegap0  10933  expgt1  10963  exprecap  10966  expmulzap  10971  leexp2a  10978  expubnd  10982  mulbinom2  11042  bernneq2  11048  expnbnd  11050  fihashss  11206  fihashssdif  11208  fimaxq  11219  ccatval2  11311  ccatass  11321  ccatw2s1leng  11351  ccat2s1fvwd  11360  swrdval  11365  swrdnd  11376  pfxfv  11401  pfxpfx  11425  ccats1pfxeq  11431  ccats1pfxeqrex  11432  s3cl  11503  s3fv0g  11508  s3fv1g  11509  s3fv2g  11510  shftuz  11527  shftfibg  11530  cjdivap  11619  resqrtcl  11739  absdivap  11780  abssubne0  11801  maxleast  11923  lemininf  11944  ltmininf  11945  xrmaxltsup  11968  xrmaxaddlem  11970  xrmaxadd  11971  xrmineqinf  11979  xrltmininf  11980  xrminltinf  11982  xrminadd  11985  climuni  12003  reccn2ap  12023  isumz  12100  geoisum1c  12231  prod1dc  12297  efltim  12409  dvdsval2  12501  dvdscmulr  12531  dvdsmulcr  12532  modmulconst  12534  dvdsadd2b  12551  dvdsexp  12572  mulmoddvds  12574  divalglemeuneg  12634  gcdaddm  12705  dvdsgcdb  12734  mulgcd  12737  gcddiv  12740  uzwodc  12758  lcmdvdsb  12806  mulgcddvds  12816  qredeq  12818  divgcdcoprm0  12823  cncongr1  12825  euclemma  12868  rpexp  12875  rpexp12i  12877  fermltl  12956  prmdiv  12957  odzcllem  12965  odzdvds  12968  odzphi  12969  vfermltl  12974  coprimeprodsq  12980  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem13  12999  pceu  13018  pcdvdsb  13043  pcgcd1  13051  dvdsprmpweq  13058  sumhashdc  13070  ctinf  13265  fvsetsid  13330  ressressg  13372  ressabsg  13373  rngplusgg  13434  imasaddvallemg  13579  qusaddvallemg  13597  plusfvalg  13626  mgmb1mgm1  13631  issubmnd  13703  ress0g  13704  imasmnd2  13707  imasmnd  13708  gsumfzz  13750  grpasscan2  13819  grpidrcan  13820  grpidlcan  13821  grpinvadd  13833  grpsubeq0  13841  grppncan  13846  dfgrp3mlem  13853  dfgrp3me  13855  grpsubpropd2  13860  imasgrp2  13863  imasgrp  13864  mhmmnd  13869  mulgnn0p1  13886  mulgnnsubcl  13887  mulgnn0subcl  13888  mulgsubcl  13889  mulgneg  13893  mulgaddcom  13899  mulginvcom  13900  submmulg  13919  subgcl  13937  subgsubcl  13938  subgsub  13939  subgmulg  13941  nsgconj  13959  nsgid  13968  quseccl0g  13984  ghmmulg  14009  ghmeqker  14024  f1ghm0to0  14025  kerf1ghm  14027  ablinvadd  14063  ablsub4  14066  ablpncan2  14069  subgabl  14085  gsumfzconst  14094  gfsumsn  14107  pwsinvg  14157  rngcl  14183  imasrng  14195  srgcl  14213  ringcl  14256  crngcom  14257  ringidss  14272  ringcom  14274  imasring  14307  opprringbg  14323  unitmulcl  14358  unitmulclb  14359  dvrcl  14380  unitdvcl  14381  dvrcan1  14385  dvrcan3  14386  rhmmul  14409  subrngrng  14448  subrngmcl  14455  subrgmcl  14479  subrgdv  14484  rrgeq0  14511  domneq0  14519  islmod  14565  scafvalg  14581  lmodcom  14607  rmodislmodlem  14624  rmodislmod  14625  lssclg  14638  lssvnegcl  14650  lssintclm  14658  lspss  14673  lspun  14676  lspsnvsi  14692  rspssp  14768  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  zndvds  14923  psrbaglecl  14950  psrbagcon  14952  2basgeng  15073  iuncld  15106  ntrss  15110  restco  15165  restabs  15166  cnprcl2k  15197  lmconst  15207  cnrest2  15227  cnmpt2t  15284  psmetsym  15320  psmetge0  15322  xmetge0  15356  xmetsym  15359  blvalps  15379  blval  15380  xblcntrps  15404  xblcntr  15405  xmssym  15460  blsscls2  15484  bdxmet  15492  txmetcnp  15509  dvfvalap  15672  dvid  15686  dvidre  15688  dvcnp2cntop  15690  elplyr  15731  rpcxpadd  15896  rpcxpsub  15899  rpmulcxp  15900  rpdivcxp  15902  cxpmul  15903  rpcxple2  15909  rpcxplt2  15910  rplogbval  15936  rplogbcl  15937  rplogbreexp  15944  relogbexpap  15949  logbleb  15952  logblt  15953  rplogbcxp  15954  rpcxplogb  15955  relogbcxpbap  15956  sgmppw  15986  lgsneg1  16024  lgsmod  16025  lgsne0  16037  lgssq  16039  lgsdirnn0  16046  lgsdinn0  16047  lgsquad  16079  funvtxvalg  16157  funiedgvalg  16158  lpvtx  16200  ausgrumgrien  16291  ausgrusgrien  16292  uhgrissubgr  16382  egrsubgr  16384  subumgredg2en  16392  subusgr  16396  wlkl1loop  16479  clwwlknonex2  16560  eulerpathprum  16601  eulerpathum  16602  findset  16841  repiecele0  16936  repiecege0  16937