Theorem simp2 982

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

Syntax hints:   -> wi 4   /\ w3a 962

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

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

This theorem is referenced by:  simpl2  985  simpr2  988  simp2i  991  simp2d  994  simp12  1012  simp22  1015  simp32  1018  syld3an3  1261  3ianorr  1287  stoic4b  1409  nlim0  4316  tfisi  4501  sotri2  4936  sotri3  4937  feq123  5264  sefvex  5442  fvmptt  5512  fnfvima  5652  cocan1  5688  cocan2  5689  ovexg  5805  ovmpox  5899  ovmpoga  5900  caovimo  5964  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfrcllembxssdm  6253  tfrcllembfn  6254  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  mapxpen  6742  dif1en  6773  diffifi  6788  unsnfidcex  6808  unfidisj  6810  undifdc  6812  resfnfinfinss  6828  funrnfi  6830  sbthlemi9  6853  elfir  6861  difinfsn  6985  ctssdc  6998  djuassen  7073  xpdjuen  7074  mulcanenq  7193  ltanqg  7208  mulcanenq0ec  7253  addnnnq0  7257  distrprg  7396  aptipr  7449  addsrpr  7553  mulsrpr  7554  mulasssrg  7566  ltpsrprg  7611  axmulass  7681  axpre-ltadd  7694  subadd2  7966  nppcan  7984  nppcan3  7986  subsub2  7990  subsub4  7995  npncan3  8000  pnpcan  8001  pnncan  8003  subcan  8017  ltadd1  8191  leadd1  8192  leadd2  8193  ltsubadd  8194  ltsubadd2  8195  lesubadd  8196  lesubadd2  8197  ltaddsub  8198  leaddsub  8200  lesub1  8218  lesub2  8219  ltsub1  8220  ltsub2  8221  gt0add  8335  apreap  8349  lemul1  8355  reapmul1lem  8356  reapmul1  8357  reapadd1  8358  remulext1  8361  remulext2  8362  apadd2  8371  mulext2  8375  mulap0r  8377  leltap  8387  ltap  8395  apsub1  8404  recexaplem2  8413  mulcanap  8426  mulcanap2  8427  divvalap  8434  divmulap  8435  divcanap1  8441  diveqap0  8442  divap0b  8443  divrecap  8448  divassap  8450  div23ap  8451  divdirap  8457  divcanap3  8458  div11ap  8460  diveqap1  8465  divmuldivap  8472  divcanap5  8474  redivclap  8491  div2negap  8495  apmul1  8548  apmul2  8549  div2subap  8596  ltdiv1  8626  ledivmul  8635  lemuldiv  8639  lt2msq1  8643  ltdiv23  8650  squeeze0  8662  zaddcllemneg  9093  eluzsub  9355  nn01to3  9409  rpgecl  9470  addlelt  9555  xleadd1  9658  xltadd1  9659  lbioog  9696  ubioc1  9712  ubicc2  9768  icoshftf1o  9774  fzen  9823  ubmelfzo  9977  ssfzo12  10001  ubmelm1fzo  10003  fzosplitprm1  10011  rebtwn2zlemshrink  10031  qbtwnre  10034  flqwordi  10061  flqword2  10062  flltdivnn0lt  10077  modqcl  10099  mulqmod0  10103  modqmulnn  10115  modqabs2  10131  modqmuladdnn0  10141  qnegmod  10142  addmodid  10145  modqm1p1mod0  10148  modifeq2int  10159  modqdi  10165  modqeqmodmin  10167  modfzo0difsn  10168  frec2uzf1od  10179  exp3val  10295  expnegap0  10301  expgt1  10331  exprecap  10334  expmulzap  10339  leexp2a  10346  expubnd  10350  mulbinom2  10408  bernneq2  10413  expnbnd  10415  fihashss  10562  fihashssdif  10564  fimaxq  10573  shftuz  10589  shftfibg  10592  cjdivap  10681  resqrtcl  10801  absdivap  10842  abssubne0  10863  maxleast  10985  lemininf  11005  ltmininf  11006  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  xrmineqinf  11038  xrltmininf  11039  xrminltinf  11041  xrminadd  11044  climuni  11062  reccn2ap  11082  isumz  11158  geoisum1c  11289  efltim  11404  dvdsval2  11496  dvdscmulr  11522  dvdsmulcr  11523  modmulconst  11525  dvdsadd2b  11540  dvdsexp  11559  mulmoddvds  11561  divalglemeuneg  11620  gcdaddm  11672  dvdsgcdb  11701  mulgcd  11704  gcddiv  11707  lcmdvdsb  11765  mulgcddvds  11775  qredeq  11777  divgcdcoprm0  11782  cncongr1  11784  euclemma  11824  rpexp  11831  rpexp12i  11833  ctinf  11943  fvsetsid  11993  ressid2  12018  ressval2  12019  rngplusgg  12076  2basgeng  12251  iuncld  12284  ntrss  12288  restco  12343  restabs  12344  cnprcl2k  12375  lmconst  12385  cnrest2  12405  cnmpt2t  12462  psmetsym  12498  psmetge0  12500  xmetge0  12534  xmetsym  12537  blvalps  12557  blval  12558  xblcntrps  12582  xblcntr  12583  xmssym  12638  blsscls2  12662  bdxmet  12670  txmetcnp  12687  dvfvalap  12819  dvid  12831  dvcnp2cntop  12832  findset  13143