Theorem simp2 939

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

Syntax hints:   -> wi 4   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl2  942  simpr2  945  simp2i  948  simp2d  951  simp12  969  simp22  972  simp32  975  syld3an3  1214  3ianorr  1240  stoic4b  1362  nlim0  4149  tfisi  4328  sotri2  4742  sotri3  4743  feq123  5058  sefvex  5216  fvmptt  5283  fnfvima  5414  cocan1  5447  cocan2  5448  ovexg  5559  ovmpt2x  5649  ovmpt2ga  5650  caovimo  5714  frecsuclem3  6013  dif1en  6364  diffifi  6378  unsnfidcex  6385  funrnfi  6392  mulcanenq  6575  ltanqg  6590  mulcanenq0ec  6635  addnnnq0  6639  distrprg  6778  aptipr  6831  addsrpr  6922  mulsrpr  6923  mulasssrg  6935  axmulass  7039  axpre-ltadd  7052  subadd2  7312  nppcan  7330  nppcan3  7332  subsub2  7336  subsub4  7341  npncan3  7346  pnpcan  7347  pnncan  7349  subcan  7363  ltadd1  7533  leadd1  7534  leadd2  7535  ltsubadd  7536  ltsubadd2  7537  lesubadd  7538  lesubadd2  7539  ltaddsub  7540  leaddsub  7542  lesub1  7560  lesub2  7561  ltsub1  7562  ltsub2  7563  gt0add  7673  apreap  7687  lemul1  7693  reapmul1lem  7694  reapmul1  7695  reapadd1  7696  remulext1  7699  remulext2  7700  apadd2  7709  mulext2  7713  mulap0r  7715  leltap  7724  ltap  7731  recexaplem2  7742  mulcanap  7755  mulcanap2  7756  divvalap  7762  divmulap  7763  divcanap1  7769  diveqap0  7770  divap0b  7771  divrecap  7776  divassap  7778  div23ap  7779  divdirap  7785  divcanap3  7786  div11ap  7788  diveqap1  7793  divmuldivap  7800  divcanap5  7802  redivclap  7819  div2negap  7823  apmul1  7876  ltdiv1  7946  ledivmul  7955  lemuldiv  7959  lt2msq1  7963  ltdiv23  7970  squeeze0  7982  zaddcllemneg  8390  eluzsub  8648  nn01to3  8702  rpgecl  8762  addlelt  8839  lbioog  8936  ubioc1  8952  ubicc2  9007  icoshftf1o  9013  fzen  9062  ubmelfzo  9209  ssfzo12  9233  ubmelm1fzo  9235  fzosplitprm1  9243  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  qbtwnre  9265  flqwordi  9290  flqword2  9291  flltdivnn0lt  9306  modqcl  9328  mulqmod0  9332  modqmulnn  9344  modqabs2  9360  modqmuladdnn0  9370  qnegmod  9371  addmodid  9374  modqm1p1mod0  9377  modifeq2int  9388  modqdi  9394  modqeqmodmin  9396  modfzo0difsn  9397  frec2uzf1od  9408  expnegap0  9484  expgt1  9514  exprecap  9517  expmulzap  9522  leexp2a  9529  expubnd  9533  mulbinom2  9589  bernneq2  9594  expnbnd  9596  shftuz  9705  shftfibg  9708  cjdivap  9796  resqrtcl  9915  absdivap  9956  abssubne0  9977  maxleast  10099  lemininf  10115  ltmininf  10116  climuni  10132  dvdsval2  10198  dvdscmulr  10224  dvdsmulcr  10225  modmulconst  10227  dvdsadd2b  10242  dvdsexp  10261  mulmoddvds  10263  divalglemeuneg  10323  gcdaddm  10375  dvdsgcdb  10402  mulgcd  10405  gcddiv  10408  lcmdvdsb  10466  mulgcddvds  10476  qredeq  10478  divgcdcoprm0  10483  cncongr1  10485  euclemma  10525  rpexp  10532  rpexp12i  10534  findset  10740