Theorem simp2 1000

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simpl2  1003  simpr2  1006  simp2i  1009  simp2d  1012  simp12  1030  simp22  1033  simp32  1036  syld3an3  1294  3ianorr  1321  intn3an2d  1368  stoic4b  1452  nlim0  4440  tfisi  4634  sotri2  5079  sotri3  5080  feq123  5416  sefvex  5596  fvmptt  5670  fnfvima  5818  cocan1  5855  cocan2  5856  ovexg  5977  ovmpox  6073  ovmpoga  6074  fvmpopr2d  6081  caovimo  6139  tfr1onlembxssdm  6428  tfr1onlembfn  6429  tfrcllembxssdm  6441  tfrcllembfn  6442  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecrdg  6493  domssr  6868  mapxpen  6944  dif1en  6975  diffifi  6990  unsnfidcex  7016  unfidisj  7018  undifdc  7020  resfnfinfinss  7040  funrnfi  7043  sbthlemi9  7066  elfir  7074  difinfsn  7201  ctssdc  7214  djuassen  7328  xpdjuen  7329  mulcanenq  7497  ltanqg  7512  mulcanenq0ec  7557  addnnnq0  7561  distrprg  7700  aptipr  7753  addsrpr  7857  mulsrpr  7858  mulasssrg  7870  ltpsrprg  7915  axmulass  7985  axpre-ltadd  7998  subadd2  8275  nppcan  8293  nppcan3  8295  subsub2  8299  subsub4  8304  npncan3  8309  pnpcan  8310  pnncan  8312  subcan  8326  ltadd1  8501  leadd1  8502  leadd2  8503  ltsubadd  8504  ltsubadd2  8505  lesubadd  8506  lesubadd2  8507  ltaddsub  8508  leaddsub  8510  lesub1  8528  lesub2  8529  ltsub1  8530  ltsub2  8531  gt0add  8645  apreap  8659  lemul1  8665  reapmul1lem  8666  reapmul1  8667  reapadd1  8668  remulext1  8671  remulext2  8672  apadd2  8681  mulext2  8685  mulap0r  8687  leltap  8697  ltap  8705  apsub1  8714  recexaplem2  8724  mulcanap  8737  mulcanap2  8738  divvalap  8746  divmulap  8747  divcanap1  8753  diveqap0  8754  divap0b  8755  divrecap  8760  divassap  8762  div23ap  8763  divdirap  8769  divcanap3  8770  div11ap  8772  diveqap1  8777  divmuldivap  8784  divcanap5  8786  redivclap  8803  div2negap  8807  apmul1  8860  apmul2  8861  div2subap  8909  ltdiv1  8940  ledivmul  8949  lemuldiv  8953  lt2msq1  8957  ltdiv23  8964  squeeze0  8976  ofnegsub  9034  zaddcllemneg  9410  eluzsub  9677  nn01to3  9737  rpgecl  9803  addlelt  9889  xleadd1  9996  xltadd1  9997  lbioog  10034  ubioc1  10050  ubicc2  10106  icoshftf1o  10112  fzen  10164  nelfzo  10273  ubmelfzo  10327  ssfzo12  10351  ubmelm1fzo  10353  fzosplitprm1  10361  zsupssdc  10379  rebtwn2zlemshrink  10394  qbtwnre  10397  icogelb  10406  flqwordi  10429  flqword2  10430  flltdivnn0lt  10445  modqcl  10469  mulqmod0  10473  modqmulnn  10485  modqabs2  10501  modqmuladdnn0  10511  qnegmod  10512  addmodid  10515  modqm1p1mod0  10518  modifeq2int  10529  modqdi  10535  modqeqmodmin  10537  modfzo0difsn  10538  frec2uzf1od  10549  exp3val  10684  expnegap0  10690  expgt1  10720  exprecap  10723  expmulzap  10728  leexp2a  10735  expubnd  10739  mulbinom2  10799  bernneq2  10804  expnbnd  10806  fihashss  10959  fihashssdif  10961  fimaxq  10970  ccatval2  11052  ccatass  11062  shftuz  11099  shftfibg  11102  cjdivap  11191  resqrtcl  11311  absdivap  11352  abssubne0  11373  maxleast  11495  lemininf  11516  ltmininf  11517  xrmaxltsup  11540  xrmaxaddlem  11542  xrmaxadd  11543  xrmineqinf  11551  xrltmininf  11552  xrminltinf  11554  xrminadd  11557  climuni  11575  reccn2ap  11595  isumz  11671  geoisum1c  11802  prod1dc  11868  efltim  11980  dvdsval2  12072  dvdscmulr  12102  dvdsmulcr  12103  modmulconst  12105  dvdsadd2b  12122  dvdsexp  12143  mulmoddvds  12145  divalglemeuneg  12205  gcdaddm  12276  dvdsgcdb  12305  mulgcd  12308  gcddiv  12311  uzwodc  12329  lcmdvdsb  12377  mulgcddvds  12387  qredeq  12389  divgcdcoprm0  12394  cncongr1  12396  euclemma  12439  rpexp  12446  rpexp12i  12448  fermltl  12527  prmdiv  12528  odzcllem  12536  odzdvds  12539  odzphi  12540  vfermltl  12545  coprimeprodsq  12551  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem12  12569  pythagtriplem13  12570  pceu  12589  pcdvdsb  12614  pcgcd1  12622  dvdsprmpweq  12629  sumhashdc  12641  ctinf  12772  fvsetsid  12837  ressressg  12878  ressabsg  12879  rngplusgg  12940  imasaddvallemg  13118  qusaddvallemg  13136  plusfvalg  13166  mgmb1mgm1  13171  issubmnd  13245  ress0g  13246  imasmnd2  13255  imasmnd  13256  gsumfzz  13298  grpasscan2  13367  grpidrcan  13368  grpidlcan  13369  grpinvadd  13381  grpsubeq0  13389  grppncan  13394  dfgrp3mlem  13401  dfgrp3me  13403  grpsubpropd2  13408  pwsinvg  13415  imasgrp2  13417  imasgrp  13418  mhmmnd  13423  mulgnn0p1  13440  mulgnnsubcl  13441  mulgnn0subcl  13442  mulgsubcl  13443  mulgneg  13447  mulgaddcom  13453  mulginvcom  13454  submmulg  13473  subgcl  13491  subgsubcl  13492  subgsub  13493  subgmulg  13495  nsgconj  13513  nsgid  13522  quseccl0g  13538  ghmmulg  13563  ghmeqker  13578  f1ghm0to0  13579  kerf1ghm  13581  ablinvadd  13617  ablsub4  13620  ablpncan2  13623  subgabl  13639  gsumfzconst  13648  rngcl  13677  imasrng  13689  srgcl  13703  ringcl  13746  crngcom  13747  ringidss  13762  ringcom  13764  imasring  13797  opprringbg  13813  unitmulcl  13846  unitmulclb  13847  dvrcl  13868  unitdvcl  13869  dvrcan1  13873  dvrcan3  13874  rhmmul  13897  subrngrng  13935  subrngmcl  13942  subrgmcl  13966  subrgdv  13971  rrgeq0  13998  domneq0  14005  islmod  14024  scafvalg  14040  lmodcom  14066  rmodislmodlem  14083  rmodislmod  14084  lssclg  14097  lssvnegcl  14109  lssintclm  14117  lspss  14132  lspun  14135  lspsnvsi  14151  rspssp  14227  rnglidlmmgm  14229  rnglidlmsgrp  14230  rnglidlrng  14231  zndvds  14382  2basgeng  14525  iuncld  14558  ntrss  14562  restco  14617  restabs  14618  cnprcl2k  14649  lmconst  14659  cnrest2  14679  cnmpt2t  14736  psmetsym  14772  psmetge0  14774  xmetge0  14808  xmetsym  14811  blvalps  14831  blval  14832  xblcntrps  14856  xblcntr  14857  xmssym  14912  blsscls2  14936  bdxmet  14944  txmetcnp  14961  dvfvalap  15124  dvid  15138  dvidre  15140  dvcnp2cntop  15142  elplyr  15183  rpcxpadd  15348  rpcxpsub  15351  rpmulcxp  15352  rpdivcxp  15354  cxpmul  15355  rpcxple2  15361  rpcxplt2  15362  rplogbval  15388  rplogbcl  15389  rplogbreexp  15396  relogbexpap  15401  logbleb  15404  logblt  15405  rplogbcxp  15406  rpcxplogb  15407  relogbcxpbap  15408  sgmppw  15435  lgsneg1  15473  lgsmod  15474  lgsne0  15486  lgssq  15488  lgsdirnn0  15495  lgsdinn0  15496  lgsquad  15528  funvtxvalg  15604  funiedgvalg  15605  findset  15843