Theorem simp2 950

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

Syntax hints:   -> wi 4   /\ w3a 930

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

This theorem depends on definitions:  df-bi 116  df-3an 932

This theorem is referenced by:  simpl2  953  simpr2  956  simp2i  959  simp2d  962  simp12  980  simp22  983  simp32  986  syld3an3  1229  3ianorr  1255  stoic4b  1377  nlim0  4254  tfisi  4439  sotri2  4872  sotri3  4873  feq123  5200  sefvex  5374  fvmptt  5444  fnfvima  5584  cocan1  5620  cocan2  5621  ovexg  5737  ovmpox  5831  ovmpoga  5832  caovimo  5896  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfrcllembxssdm  6183  tfrcllembfn  6184  freccllem  6229  frecfcllem  6231  frecsuclem  6233  frecrdg  6235  mapxpen  6671  dif1en  6702  diffifi  6717  unsnfidcex  6737  unfidisj  6739  undifdc  6741  resfnfinfinss  6756  funrnfi  6758  sbthlemi9  6781  difinfsn  6900  ctssdc  6912  djuassen  6977  xpdjuen  6978  mulcanenq  7094  ltanqg  7109  mulcanenq0ec  7154  addnnnq0  7158  distrprg  7297  aptipr  7350  addsrpr  7441  mulsrpr  7442  mulasssrg  7454  axmulass  7558  axpre-ltadd  7571  subadd2  7837  nppcan  7855  nppcan3  7857  subsub2  7861  subsub4  7866  npncan3  7871  pnpcan  7872  pnncan  7874  subcan  7888  ltadd1  8058  leadd1  8059  leadd2  8060  ltsubadd  8061  ltsubadd2  8062  lesubadd  8063  lesubadd2  8064  ltaddsub  8065  leaddsub  8067  lesub1  8085  lesub2  8086  ltsub1  8087  ltsub2  8088  gt0add  8201  apreap  8215  lemul1  8221  reapmul1lem  8222  reapmul1  8223  reapadd1  8224  remulext1  8227  remulext2  8228  apadd2  8237  mulext2  8241  mulap0r  8243  leltap  8253  ltap  8260  apsub1  8269  recexaplem2  8274  mulcanap  8287  mulcanap2  8288  divvalap  8295  divmulap  8296  divcanap1  8302  diveqap0  8303  divap0b  8304  divrecap  8309  divassap  8311  div23ap  8312  divdirap  8318  divcanap3  8319  div11ap  8321  diveqap1  8326  divmuldivap  8333  divcanap5  8335  redivclap  8352  div2negap  8356  apmul1  8409  apmul2  8410  div2subap  8457  ltdiv1  8484  ledivmul  8493  lemuldiv  8497  lt2msq1  8501  ltdiv23  8508  squeeze0  8520  zaddcllemneg  8945  eluzsub  9205  nn01to3  9259  rpgecl  9319  addlelt  9396  xleadd1  9499  xltadd1  9500  lbioog  9537  ubioc1  9553  ubicc2  9609  icoshftf1o  9615  fzen  9664  ubmelfzo  9818  ssfzo12  9842  ubmelm1fzo  9844  fzosplitprm1  9852  rebtwn2zlemshrink  9872  qbtwnre  9875  flqwordi  9902  flqword2  9903  flltdivnn0lt  9918  modqcl  9940  mulqmod0  9944  modqmulnn  9956  modqabs2  9972  modqmuladdnn0  9982  qnegmod  9983  addmodid  9986  modqm1p1mod0  9989  modifeq2int  10000  modqdi  10006  modqeqmodmin  10008  modfzo0difsn  10009  frec2uzf1od  10020  exp3val  10136  expnegap0  10142  expgt1  10172  exprecap  10175  expmulzap  10180  leexp2a  10187  expubnd  10191  mulbinom2  10249  bernneq2  10254  expnbnd  10256  fihashss  10403  fihashssdif  10405  fimaxq  10414  shftuz  10430  shftfibg  10433  cjdivap  10522  resqrtcl  10641  absdivap  10682  abssubne0  10703  maxleast  10825  lemininf  10844  ltmininf  10845  xrmaxltsup  10866  xrmaxaddlem  10868  xrmaxadd  10869  xrmineqinf  10877  xrltmininf  10878  xrminltinf  10880  xrminadd  10883  climuni  10901  reccn2ap  10921  isumz  10997  geoisum1c  11128  efltim  11202  dvdsval2  11291  dvdscmulr  11317  dvdsmulcr  11318  modmulconst  11320  dvdsadd2b  11335  dvdsexp  11354  mulmoddvds  11356  divalglemeuneg  11415  gcdaddm  11467  dvdsgcdb  11494  mulgcd  11497  gcddiv  11500  lcmdvdsb  11558  mulgcddvds  11568  qredeq  11570  divgcdcoprm0  11575  cncongr1  11577  euclemma  11617  rpexp  11624  rpexp12i  11626  ctinf  11735  fvsetsid  11775  ressid2  11800  ressval2  11801  rngplusgg  11858  2basgeng  12033  iuncld  12066  ntrss  12070  restco  12125  restabs  12126  cnprcl2k  12156  lmconst  12166  cnrest2  12186  cnmpt2t  12243  psmetsym  12257  psmetge0  12259  xmetge0  12293  xmetsym  12296  blvalps  12316  blval  12317  xblcntrps  12341  xblcntr  12342  xmssym  12397  blsscls2  12421  bdxmet  12429  dvfvalap  12523  dvid  12535  findset  12728