Theorem simp2 987

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

Syntax hints:   -> wi 4   /\ w3a 967

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 969

This theorem is referenced by:  simpl2  990  simpr2  993  simp2i  996  simp2d  999  simp12  1017  simp22  1020  simp32  1023  syld3an3  1272  3ianorr  1298  stoic4b  1420  nlim0  4366  tfisi  4558  sotri2  4995  sotri3  4996  feq123  5323  sefvex  5501  fvmptt  5571  fnfvima  5713  cocan1  5749  cocan2  5750  ovexg  5867  ovmpox  5961  ovmpoga  5962  caovimo  6026  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfrcllembxssdm  6315  tfrcllembfn  6316  freccllem  6361  frecfcllem  6363  frecsuclem  6365  frecrdg  6367  mapxpen  6805  dif1en  6836  diffifi  6851  unsnfidcex  6876  unfidisj  6878  undifdc  6880  resfnfinfinss  6896  funrnfi  6898  sbthlemi9  6921  elfir  6929  difinfsn  7056  ctssdc  7069  djuassen  7164  xpdjuen  7165  mulcanenq  7317  ltanqg  7332  mulcanenq0ec  7377  addnnnq0  7381  distrprg  7520  aptipr  7573  addsrpr  7677  mulsrpr  7678  mulasssrg  7690  ltpsrprg  7735  axmulass  7805  axpre-ltadd  7818  subadd2  8093  nppcan  8111  nppcan3  8113  subsub2  8117  subsub4  8122  npncan3  8127  pnpcan  8128  pnncan  8130  subcan  8144  ltadd1  8318  leadd1  8319  leadd2  8320  ltsubadd  8321  ltsubadd2  8322  lesubadd  8323  lesubadd2  8324  ltaddsub  8325  leaddsub  8327  lesub1  8345  lesub2  8346  ltsub1  8347  ltsub2  8348  gt0add  8462  apreap  8476  lemul1  8482  reapmul1lem  8483  reapmul1  8484  reapadd1  8485  remulext1  8488  remulext2  8489  apadd2  8498  mulext2  8502  mulap0r  8504  leltap  8514  ltap  8522  apsub1  8531  recexaplem2  8540  mulcanap  8553  mulcanap2  8554  divvalap  8561  divmulap  8562  divcanap1  8568  diveqap0  8569  divap0b  8570  divrecap  8575  divassap  8577  div23ap  8578  divdirap  8584  divcanap3  8585  div11ap  8587  diveqap1  8592  divmuldivap  8599  divcanap5  8601  redivclap  8618  div2negap  8622  apmul1  8675  apmul2  8676  div2subap  8724  ltdiv1  8754  ledivmul  8763  lemuldiv  8767  lt2msq1  8771  ltdiv23  8778  squeeze0  8790  zaddcllemneg  9221  eluzsub  9486  nn01to3  9546  rpgecl  9609  addlelt  9695  xleadd1  9802  xltadd1  9803  lbioog  9840  ubioc1  9856  ubicc2  9912  icoshftf1o  9918  fzen  9968  ubmelfzo  10125  ssfzo12  10149  ubmelm1fzo  10151  fzosplitprm1  10159  rebtwn2zlemshrink  10179  qbtwnre  10182  icogelb  10191  flqwordi  10213  flqword2  10214  flltdivnn0lt  10229  modqcl  10251  mulqmod0  10255  modqmulnn  10267  modqabs2  10283  modqmuladdnn0  10293  qnegmod  10294  addmodid  10297  modqm1p1mod0  10300  modifeq2int  10311  modqdi  10317  modqeqmodmin  10319  modfzo0difsn  10320  frec2uzf1od  10331  exp3val  10447  expnegap0  10453  expgt1  10483  exprecap  10486  expmulzap  10491  leexp2a  10498  expubnd  10502  mulbinom2  10560  bernneq2  10565  expnbnd  10567  fihashss  10718  fihashssdif  10720  fimaxq  10729  shftuz  10745  shftfibg  10748  cjdivap  10837  resqrtcl  10957  absdivap  10998  abssubne0  11019  maxleast  11141  lemininf  11161  ltmininf  11162  xrmaxltsup  11185  xrmaxaddlem  11187  xrmaxadd  11188  xrmineqinf  11196  xrltmininf  11197  xrminltinf  11199  xrminadd  11202  climuni  11220  reccn2ap  11240  isumz  11316  geoisum1c  11447  prod1dc  11513  efltim  11625  dvdsval2  11716  dvdscmulr  11746  dvdsmulcr  11747  modmulconst  11749  dvdsadd2b  11765  dvdsexp  11784  mulmoddvds  11786  divalglemeuneg  11845  zsupssdc  11872  gcdaddm  11902  dvdsgcdb  11931  mulgcd  11934  gcddiv  11937  lcmdvdsb  11995  mulgcddvds  12005  qredeq  12007  divgcdcoprm0  12012  cncongr1  12014  euclemma  12055  rpexp  12062  rpexp12i  12064  fermltl  12143  prmdiv  12144  odzcllem  12151  odzdvds  12154  odzphi  12155  vfermltl  12160  coprimeprodsq  12166  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem12  12184  pythagtriplem13  12185  pceu  12204  pcdvdsb  12228  pcgcd1  12236  dvdsprmpweq  12243  sumhashdc  12254  ctinf  12300  fvsetsid  12365  ressid2  12390  ressval2  12391  rngplusgg  12448  2basgeng  12623  iuncld  12656  ntrss  12660  restco  12715  restabs  12716  cnprcl2k  12747  lmconst  12757  cnrest2  12777  cnmpt2t  12834  psmetsym  12870  psmetge0  12872  xmetge0  12906  xmetsym  12909  blvalps  12929  blval  12930  xblcntrps  12954  xblcntr  12955  xmssym  13010  blsscls2  13034  bdxmet  13042  txmetcnp  13059  dvfvalap  13191  dvid  13203  dvcnp2cntop  13204  rpcxpadd  13367  rpcxpsub  13370  rpmulcxp  13371  rpdivcxp  13373  cxpmul  13374  rpcxple2  13379  rpcxplt2  13380  rplogbval  13404  rplogbcl  13405  rplogbreexp  13412  relogbexpap  13417  logbleb  13420  logblt  13421  rplogbcxp  13422  rpcxplogb  13423  relogbcxpbap  13424  findset  13662