Theorem simp2 998

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

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

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

This theorem is referenced by:  simpl2  1001  simpr2  1004  simp2i  1007  simp2d  1010  simp12  1028  simp22  1031  simp32  1034  syld3an3  1283  3ianorr  1309  stoic4b  1433  nlim0  4396  tfisi  4588  sotri2  5028  sotri3  5029  feq123  5359  sefvex  5538  fvmptt  5609  fnfvima  5753  cocan1  5790  cocan2  5791  ovexg  5911  ovmpox  6005  ovmpoga  6006  caovimo  6070  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfrcllembxssdm  6359  tfrcllembfn  6360  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecrdg  6411  mapxpen  6850  dif1en  6881  diffifi  6896  unsnfidcex  6921  unfidisj  6923  undifdc  6925  resfnfinfinss  6941  funrnfi  6943  sbthlemi9  6966  elfir  6974  difinfsn  7101  ctssdc  7114  djuassen  7218  xpdjuen  7219  mulcanenq  7386  ltanqg  7401  mulcanenq0ec  7446  addnnnq0  7450  distrprg  7589  aptipr  7642  addsrpr  7746  mulsrpr  7747  mulasssrg  7759  ltpsrprg  7804  axmulass  7874  axpre-ltadd  7887  subadd2  8163  nppcan  8181  nppcan3  8183  subsub2  8187  subsub4  8192  npncan3  8197  pnpcan  8198  pnncan  8200  subcan  8214  ltadd1  8388  leadd1  8389  leadd2  8390  ltsubadd  8391  ltsubadd2  8392  lesubadd  8393  lesubadd2  8394  ltaddsub  8395  leaddsub  8397  lesub1  8415  lesub2  8416  ltsub1  8417  ltsub2  8418  gt0add  8532  apreap  8546  lemul1  8552  reapmul1lem  8553  reapmul1  8554  reapadd1  8555  remulext1  8558  remulext2  8559  apadd2  8568  mulext2  8572  mulap0r  8574  leltap  8584  ltap  8592  apsub1  8601  recexaplem2  8611  mulcanap  8624  mulcanap2  8625  divvalap  8633  divmulap  8634  divcanap1  8640  diveqap0  8641  divap0b  8642  divrecap  8647  divassap  8649  div23ap  8650  divdirap  8656  divcanap3  8657  div11ap  8659  diveqap1  8664  divmuldivap  8671  divcanap5  8673  redivclap  8690  div2negap  8694  apmul1  8747  apmul2  8748  div2subap  8796  ltdiv1  8827  ledivmul  8836  lemuldiv  8840  lt2msq1  8844  ltdiv23  8851  squeeze0  8863  zaddcllemneg  9294  eluzsub  9559  nn01to3  9619  rpgecl  9684  addlelt  9770  xleadd1  9877  xltadd1  9878  lbioog  9915  ubioc1  9931  ubicc2  9987  icoshftf1o  9993  fzen  10045  ubmelfzo  10202  ssfzo12  10226  ubmelm1fzo  10228  fzosplitprm1  10236  rebtwn2zlemshrink  10256  qbtwnre  10259  icogelb  10268  flqwordi  10290  flqword2  10291  flltdivnn0lt  10306  modqcl  10328  mulqmod0  10332  modqmulnn  10344  modqabs2  10360  modqmuladdnn0  10370  qnegmod  10371  addmodid  10374  modqm1p1mod0  10377  modifeq2int  10388  modqdi  10394  modqeqmodmin  10396  modfzo0difsn  10397  frec2uzf1od  10408  exp3val  10524  expnegap0  10530  expgt1  10560  exprecap  10563  expmulzap  10568  leexp2a  10575  expubnd  10579  mulbinom2  10639  bernneq2  10644  expnbnd  10646  fihashss  10798  fihashssdif  10800  fimaxq  10809  shftuz  10828  shftfibg  10831  cjdivap  10920  resqrtcl  11040  absdivap  11081  abssubne0  11102  maxleast  11224  lemininf  11244  ltmininf  11245  xrmaxltsup  11268  xrmaxaddlem  11270  xrmaxadd  11271  xrmineqinf  11279  xrltmininf  11280  xrminltinf  11282  xrminadd  11285  climuni  11303  reccn2ap  11323  isumz  11399  geoisum1c  11530  prod1dc  11596  efltim  11708  dvdsval2  11799  dvdscmulr  11829  dvdsmulcr  11830  modmulconst  11832  dvdsadd2b  11849  dvdsexp  11869  mulmoddvds  11871  divalglemeuneg  11930  zsupssdc  11957  gcdaddm  11987  dvdsgcdb  12016  mulgcd  12019  gcddiv  12022  uzwodc  12040  lcmdvdsb  12086  mulgcddvds  12096  qredeq  12098  divgcdcoprm0  12103  cncongr1  12105  euclemma  12148  rpexp  12155  rpexp12i  12157  fermltl  12236  prmdiv  12237  odzcllem  12244  odzdvds  12247  odzphi  12248  vfermltl  12253  coprimeprodsq  12259  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem12  12277  pythagtriplem13  12278  pceu  12297  pcdvdsb  12321  pcgcd1  12329  dvdsprmpweq  12336  sumhashdc  12347  ctinf  12433  fvsetsid  12498  ressressg  12536  ressabsg  12537  rngplusgg  12597  imasaddvallemg  12741  qusaddvallemg  12757  plusfvalg  12787  mgmb1mgm1  12792  issubmnd  12848  ress0g  12849  grpasscan2  12939  grpidrcan  12940  grpidlcan  12941  grpinvadd  12953  grpsubeq0  12961  grppncan  12966  dfgrp3mlem  12973  dfgrp3me  12975  grpsubpropd2  12980  mhmmnd  12985  mulgnn0p1  12999  mulgnnsubcl  13000  mulgnn0subcl  13001  mulgsubcl  13002  mulgneg  13006  mulgaddcom  13012  mulginvcom  13013  subgcl  13049  subgsubcl  13050  subgsub  13051  subgmulg  13053  nsgconj  13071  nsgid  13080  ablinvadd  13118  ablsub4  13121  ablpncan2  13124  srgcl  13158  ringcl  13201  crngcom  13202  ringidss  13217  ringcom  13219  opprringbg  13255  unitmulcl  13287  unitmulclb  13288  dvrcl  13309  unitdvcl  13310  dvrcan1  13314  dvrcan3  13315  subrgmcl  13359  subrgdv  13364  islmod  13386  scafvalg  13402  lmodcom  13428  rmodislmodlem  13445  rmodislmod  13446  lssclg  13456  lssvnegcl  13468  lssintclm  13476  2basgeng  13621  iuncld  13654  ntrss  13658  restco  13713  restabs  13714  cnprcl2k  13745  lmconst  13755  cnrest2  13775  cnmpt2t  13832  psmetsym  13868  psmetge0  13870  xmetge0  13904  xmetsym  13907  blvalps  13927  blval  13928  xblcntrps  13952  xblcntr  13953  xmssym  14008  blsscls2  14032  bdxmet  14040  txmetcnp  14057  dvfvalap  14189  dvid  14201  dvcnp2cntop  14202  rpcxpadd  14365  rpcxpsub  14368  rpmulcxp  14369  rpdivcxp  14371  cxpmul  14372  rpcxple2  14377  rpcxplt2  14378  rplogbval  14402  rplogbcl  14403  rplogbreexp  14410  relogbexpap  14415  logbleb  14418  logblt  14419  rplogbcxp  14420  rpcxplogb  14421  relogbcxpbap  14422  lgsneg1  14465  lgsmod  14466  lgsne0  14478  lgssq  14480  lgsdirnn0  14487  lgsdinn0  14488  findset  14736