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  1320  stoic4b  1444  nlim0  4426  tfisi  4620  sotri2  5064  sotri3  5065  feq123  5396  sefvex  5576  fvmptt  5650  fnfvima  5794  cocan1  5831  cocan2  5832  ovexg  5953  ovmpox  6048  ovmpoga  6049  fvmpopr2d  6056  caovimo  6114  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfrcllembxssdm  6411  tfrcllembfn  6412  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecrdg  6463  mapxpen  6906  dif1en  6937  diffifi  6952  unsnfidcex  6978  unfidisj  6980  undifdc  6982  resfnfinfinss  7000  funrnfi  7003  sbthlemi9  7026  elfir  7034  difinfsn  7161  ctssdc  7174  djuassen  7279  xpdjuen  7280  mulcanenq  7447  ltanqg  7462  mulcanenq0ec  7507  addnnnq0  7511  distrprg  7650  aptipr  7703  addsrpr  7807  mulsrpr  7808  mulasssrg  7820  ltpsrprg  7865  axmulass  7935  axpre-ltadd  7948  subadd2  8225  nppcan  8243  nppcan3  8245  subsub2  8249  subsub4  8254  npncan3  8259  pnpcan  8260  pnncan  8262  subcan  8276  ltadd1  8450  leadd1  8451  leadd2  8452  ltsubadd  8453  ltsubadd2  8454  lesubadd  8455  lesubadd2  8456  ltaddsub  8457  leaddsub  8459  lesub1  8477  lesub2  8478  ltsub1  8479  ltsub2  8480  gt0add  8594  apreap  8608  lemul1  8614  reapmul1lem  8615  reapmul1  8616  reapadd1  8617  remulext1  8620  remulext2  8621  apadd2  8630  mulext2  8634  mulap0r  8636  leltap  8646  ltap  8654  apsub1  8663  recexaplem2  8673  mulcanap  8686  mulcanap2  8687  divvalap  8695  divmulap  8696  divcanap1  8702  diveqap0  8703  divap0b  8704  divrecap  8709  divassap  8711  div23ap  8712  divdirap  8718  divcanap3  8719  div11ap  8721  diveqap1  8726  divmuldivap  8733  divcanap5  8735  redivclap  8752  div2negap  8756  apmul1  8809  apmul2  8810  div2subap  8858  ltdiv1  8889  ledivmul  8898  lemuldiv  8902  lt2msq1  8906  ltdiv23  8913  squeeze0  8925  ofnegsub  8983  zaddcllemneg  9359  eluzsub  9625  nn01to3  9685  rpgecl  9751  addlelt  9837  xleadd1  9944  xltadd1  9945  lbioog  9982  ubioc1  9998  ubicc2  10054  icoshftf1o  10060  fzen  10112  nelfzo  10221  ubmelfzo  10270  ssfzo12  10294  ubmelm1fzo  10296  fzosplitprm1  10304  rebtwn2zlemshrink  10325  qbtwnre  10328  icogelb  10337  flqwordi  10360  flqword2  10361  flltdivnn0lt  10376  modqcl  10400  mulqmod0  10404  modqmulnn  10416  modqabs2  10432  modqmuladdnn0  10442  qnegmod  10443  addmodid  10446  modqm1p1mod0  10449  modifeq2int  10460  modqdi  10466  modqeqmodmin  10468  modfzo0difsn  10469  frec2uzf1od  10480  exp3val  10615  expnegap0  10621  expgt1  10651  exprecap  10654  expmulzap  10659  leexp2a  10666  expubnd  10670  mulbinom2  10730  bernneq2  10735  expnbnd  10737  fihashss  10890  fihashssdif  10892  fimaxq  10901  shftuz  10964  shftfibg  10967  cjdivap  11056  resqrtcl  11176  absdivap  11217  abssubne0  11238  maxleast  11360  lemininf  11380  ltmininf  11381  xrmaxltsup  11404  xrmaxaddlem  11406  xrmaxadd  11407  xrmineqinf  11415  xrltmininf  11416  xrminltinf  11418  xrminadd  11421  climuni  11439  reccn2ap  11459  isumz  11535  geoisum1c  11666  prod1dc  11732  efltim  11844  dvdsval2  11936  dvdscmulr  11966  dvdsmulcr  11967  modmulconst  11969  dvdsadd2b  11986  dvdsexp  12006  mulmoddvds  12008  divalglemeuneg  12067  zsupssdc  12094  gcdaddm  12124  dvdsgcdb  12153  mulgcd  12156  gcddiv  12159  uzwodc  12177  lcmdvdsb  12225  mulgcddvds  12235  qredeq  12237  divgcdcoprm0  12242  cncongr1  12244  euclemma  12287  rpexp  12294  rpexp12i  12296  fermltl  12375  prmdiv  12376  odzcllem  12383  odzdvds  12386  odzphi  12387  vfermltl  12392  coprimeprodsq  12398  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem13  12417  pceu  12436  pcdvdsb  12461  pcgcd1  12469  dvdsprmpweq  12476  sumhashdc  12488  ctinf  12590  fvsetsid  12655  ressressg  12696  ressabsg  12697  rngplusgg  12757  imasaddvallemg  12901  qusaddvallemg  12919  plusfvalg  12949  mgmb1mgm1  12954  issubmnd  13026  ress0g  13027  gsumfzz  13070  grpasscan2  13139  grpidrcan  13140  grpidlcan  13141  grpinvadd  13153  grpsubeq0  13161  grppncan  13166  dfgrp3mlem  13173  dfgrp3me  13175  grpsubpropd2  13180  imasgrp2  13183  imasgrp  13184  mhmmnd  13189  mulgnn0p1  13206  mulgnnsubcl  13207  mulgnn0subcl  13208  mulgsubcl  13209  mulgneg  13213  mulgaddcom  13219  mulginvcom  13220  submmulg  13239  subgcl  13257  subgsubcl  13258  subgsub  13259  subgmulg  13261  nsgconj  13279  nsgid  13288  quseccl0g  13304  ghmmulg  13329  ghmeqker  13344  f1ghm0to0  13345  kerf1ghm  13347  ablinvadd  13383  ablsub4  13386  ablpncan2  13389  subgabl  13405  gsumfzconst  13414  rngcl  13443  imasrng  13455  srgcl  13469  ringcl  13512  crngcom  13513  ringidss  13528  ringcom  13530  imasring  13563  opprringbg  13579  unitmulcl  13612  unitmulclb  13613  dvrcl  13634  unitdvcl  13635  dvrcan1  13639  dvrcan3  13640  rhmmul  13663  subrngrng  13701  subrngmcl  13708  subrgmcl  13732  subrgdv  13737  rrgeq0  13764  domneq0  13771  islmod  13790  scafvalg  13806  lmodcom  13832  rmodislmodlem  13849  rmodislmod  13850  lssclg  13863  lssvnegcl  13875  lssintclm  13883  lspss  13898  lspun  13901  lspsnvsi  13917  rspssp  13993  rnglidlmmgm  13995  rnglidlmsgrp  13996  rnglidlrng  13997  zndvds  14148  2basgeng  14261  iuncld  14294  ntrss  14298  restco  14353  restabs  14354  cnprcl2k  14385  lmconst  14395  cnrest2  14415  cnmpt2t  14472  psmetsym  14508  psmetge0  14510  xmetge0  14544  xmetsym  14547  blvalps  14567  blval  14568  xblcntrps  14592  xblcntr  14593  xmssym  14648  blsscls2  14672  bdxmet  14680  txmetcnp  14697  dvfvalap  14860  dvid  14874  dvidre  14876  dvcnp2cntop  14878  elplyr  14919  rpcxpadd  15081  rpcxpsub  15084  rpmulcxp  15085  rpdivcxp  15087  cxpmul  15088  rpcxple2  15093  rpcxplt2  15094  rplogbval  15118  rplogbcl  15119  rplogbreexp  15126  relogbexpap  15131  logbleb  15134  logblt  15135  rplogbcxp  15136  rpcxplogb  15137  relogbcxpbap  15138  lgsneg1  15182  lgsmod  15183  lgsne0  15195  lgssq  15197  lgsdirnn0  15204  lgsdinn0  15205  lgsquad  15237  findset  15507