Theorem simp2 988

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  simpl2  991  simpr2  994  simp2i  997  simp2d  1000  simp12  1018  simp22  1021  simp32  1024  syld3an3  1273  3ianorr  1299  stoic4b  1421  nlim0  4372  tfisi  4564  sotri2  5001  sotri3  5002  feq123  5329  sefvex  5507  fvmptt  5577  fnfvima  5719  cocan1  5755  cocan2  5756  ovexg  5876  ovmpox  5970  ovmpoga  5971  caovimo  6035  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfrcllembxssdm  6324  tfrcllembfn  6325  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecrdg  6376  mapxpen  6814  dif1en  6845  diffifi  6860  unsnfidcex  6885  unfidisj  6887  undifdc  6889  resfnfinfinss  6905  funrnfi  6907  sbthlemi9  6930  elfir  6938  difinfsn  7065  ctssdc  7078  djuassen  7173  xpdjuen  7174  mulcanenq  7326  ltanqg  7341  mulcanenq0ec  7386  addnnnq0  7390  distrprg  7529  aptipr  7582  addsrpr  7686  mulsrpr  7687  mulasssrg  7699  ltpsrprg  7744  axmulass  7814  axpre-ltadd  7827  subadd2  8102  nppcan  8120  nppcan3  8122  subsub2  8126  subsub4  8131  npncan3  8136  pnpcan  8137  pnncan  8139  subcan  8153  ltadd1  8327  leadd1  8328  leadd2  8329  ltsubadd  8330  ltsubadd2  8331  lesubadd  8332  lesubadd2  8333  ltaddsub  8334  leaddsub  8336  lesub1  8354  lesub2  8355  ltsub1  8356  ltsub2  8357  gt0add  8471  apreap  8485  lemul1  8491  reapmul1lem  8492  reapmul1  8493  reapadd1  8494  remulext1  8497  remulext2  8498  apadd2  8507  mulext2  8511  mulap0r  8513  leltap  8523  ltap  8531  apsub1  8540  recexaplem2  8549  mulcanap  8562  mulcanap2  8563  divvalap  8570  divmulap  8571  divcanap1  8577  diveqap0  8578  divap0b  8579  divrecap  8584  divassap  8586  div23ap  8587  divdirap  8593  divcanap3  8594  div11ap  8596  diveqap1  8601  divmuldivap  8608  divcanap5  8610  redivclap  8627  div2negap  8631  apmul1  8684  apmul2  8685  div2subap  8733  ltdiv1  8763  ledivmul  8772  lemuldiv  8776  lt2msq1  8780  ltdiv23  8787  squeeze0  8799  zaddcllemneg  9230  eluzsub  9495  nn01to3  9555  rpgecl  9618  addlelt  9704  xleadd1  9811  xltadd1  9812  lbioog  9849  ubioc1  9865  ubicc2  9921  icoshftf1o  9927  fzen  9978  ubmelfzo  10135  ssfzo12  10159  ubmelm1fzo  10161  fzosplitprm1  10169  rebtwn2zlemshrink  10189  qbtwnre  10192  icogelb  10201  flqwordi  10223  flqword2  10224  flltdivnn0lt  10239  modqcl  10261  mulqmod0  10265  modqmulnn  10277  modqabs2  10293  modqmuladdnn0  10303  qnegmod  10304  addmodid  10307  modqm1p1mod0  10310  modifeq2int  10321  modqdi  10327  modqeqmodmin  10329  modfzo0difsn  10330  frec2uzf1od  10341  exp3val  10457  expnegap0  10463  expgt1  10493  exprecap  10496  expmulzap  10501  leexp2a  10508  expubnd  10512  mulbinom2  10571  bernneq2  10576  expnbnd  10578  fihashss  10729  fihashssdif  10731  fimaxq  10740  shftuz  10759  shftfibg  10762  cjdivap  10851  resqrtcl  10971  absdivap  11012  abssubne0  11033  maxleast  11155  lemininf  11175  ltmininf  11176  xrmaxltsup  11199  xrmaxaddlem  11201  xrmaxadd  11202  xrmineqinf  11210  xrltmininf  11211  xrminltinf  11213  xrminadd  11216  climuni  11234  reccn2ap  11254  isumz  11330  geoisum1c  11461  prod1dc  11527  efltim  11639  dvdsval2  11730  dvdscmulr  11760  dvdsmulcr  11761  modmulconst  11763  dvdsadd2b  11780  dvdsexp  11799  mulmoddvds  11801  divalglemeuneg  11860  zsupssdc  11887  gcdaddm  11917  dvdsgcdb  11946  mulgcd  11949  gcddiv  11952  uzwodc  11970  lcmdvdsb  12016  mulgcddvds  12026  qredeq  12028  divgcdcoprm0  12033  cncongr1  12035  euclemma  12078  rpexp  12085  rpexp12i  12087  fermltl  12166  prmdiv  12167  odzcllem  12174  odzdvds  12177  odzphi  12178  vfermltl  12183  coprimeprodsq  12189  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem12  12207  pythagtriplem13  12208  pceu  12227  pcdvdsb  12251  pcgcd1  12259  dvdsprmpweq  12266  sumhashdc  12277  ctinf  12363  fvsetsid  12428  ressid2  12454  ressval2  12455  rngplusgg  12512  plusfvalg  12594  mgmb1mgm1  12599  2basgeng  12722  iuncld  12755  ntrss  12759  restco  12814  restabs  12815  cnprcl2k  12846  lmconst  12856  cnrest2  12876  cnmpt2t  12933  psmetsym  12969  psmetge0  12971  xmetge0  13005  xmetsym  13008  blvalps  13028  blval  13029  xblcntrps  13053  xblcntr  13054  xmssym  13109  blsscls2  13133  bdxmet  13141  txmetcnp  13158  dvfvalap  13290  dvid  13302  dvcnp2cntop  13303  rpcxpadd  13466  rpcxpsub  13469  rpmulcxp  13470  rpdivcxp  13472  cxpmul  13473  rpcxple2  13478  rpcxplt2  13479  rplogbval  13503  rplogbcl  13504  rplogbreexp  13511  relogbexpap  13516  logbleb  13519  logblt  13520  rplogbcxp  13521  rpcxplogb  13522  relogbcxpbap  13523  lgsneg1  13566  lgsmod  13567  lgsne0  13579  lgssq  13581  lgsdirnn0  13588  lgsdinn0  13589  findset  13827