Theorem simp2 1000

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

Syntax hints:   -> wi 4   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpl2  1003  simpr2  1006  simp2i  1009  simp2d  1012  simp12  1030  simp22  1033  simp32  1036  syld3an3  1294  3ianorr  1320  stoic4b  1444  nlim0  4425  tfisi  4619  sotri2  5063  sotri3  5064  feq123  5395  sefvex  5575  fvmptt  5649  fnfvima  5793  cocan1  5830  cocan2  5831  ovexg  5952  ovmpox  6047  ovmpoga  6048  caovimo  6112  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfrcllembxssdm  6409  tfrcllembfn  6410  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecrdg  6461  mapxpen  6904  dif1en  6935  diffifi  6950  unsnfidcex  6976  unfidisj  6978  undifdc  6980  resfnfinfinss  6998  funrnfi  7001  sbthlemi9  7024  elfir  7032  difinfsn  7159  ctssdc  7172  djuassen  7277  xpdjuen  7278  mulcanenq  7445  ltanqg  7460  mulcanenq0ec  7505  addnnnq0  7509  distrprg  7648  aptipr  7701  addsrpr  7805  mulsrpr  7806  mulasssrg  7818  ltpsrprg  7863  axmulass  7933  axpre-ltadd  7946  subadd2  8223  nppcan  8241  nppcan3  8243  subsub2  8247  subsub4  8252  npncan3  8257  pnpcan  8258  pnncan  8260  subcan  8274  ltadd1  8448  leadd1  8449  leadd2  8450  ltsubadd  8451  ltsubadd2  8452  lesubadd  8453  lesubadd2  8454  ltaddsub  8455  leaddsub  8457  lesub1  8475  lesub2  8476  ltsub1  8477  ltsub2  8478  gt0add  8592  apreap  8606  lemul1  8612  reapmul1lem  8613  reapmul1  8614  reapadd1  8615  remulext1  8618  remulext2  8619  apadd2  8628  mulext2  8632  mulap0r  8634  leltap  8644  ltap  8652  apsub1  8661  recexaplem2  8671  mulcanap  8684  mulcanap2  8685  divvalap  8693  divmulap  8694  divcanap1  8700  diveqap0  8701  divap0b  8702  divrecap  8707  divassap  8709  div23ap  8710  divdirap  8716  divcanap3  8717  div11ap  8719  diveqap1  8724  divmuldivap  8731  divcanap5  8733  redivclap  8750  div2negap  8754  apmul1  8807  apmul2  8808  div2subap  8856  ltdiv1  8887  ledivmul  8896  lemuldiv  8900  lt2msq1  8904  ltdiv23  8911  squeeze0  8923  ofnegsub  8981  zaddcllemneg  9356  eluzsub  9622  nn01to3  9682  rpgecl  9748  addlelt  9834  xleadd1  9941  xltadd1  9942  lbioog  9979  ubioc1  9995  ubicc2  10051  icoshftf1o  10057  fzen  10109  nelfzo  10218  ubmelfzo  10267  ssfzo12  10291  ubmelm1fzo  10293  fzosplitprm1  10301  rebtwn2zlemshrink  10322  qbtwnre  10325  icogelb  10334  flqwordi  10357  flqword2  10358  flltdivnn0lt  10373  modqcl  10397  mulqmod0  10401  modqmulnn  10413  modqabs2  10429  modqmuladdnn0  10439  qnegmod  10440  addmodid  10443  modqm1p1mod0  10446  modifeq2int  10457  modqdi  10463  modqeqmodmin  10465  modfzo0difsn  10466  frec2uzf1od  10477  exp3val  10612  expnegap0  10618  expgt1  10648  exprecap  10651  expmulzap  10656  leexp2a  10663  expubnd  10667  mulbinom2  10727  bernneq2  10732  expnbnd  10734  fihashss  10887  fihashssdif  10889  fimaxq  10898  shftuz  10961  shftfibg  10964  cjdivap  11053  resqrtcl  11173  absdivap  11214  abssubne0  11235  maxleast  11357  lemininf  11377  ltmininf  11378  xrmaxltsup  11401  xrmaxaddlem  11403  xrmaxadd  11404  xrmineqinf  11412  xrltmininf  11413  xrminltinf  11415  xrminadd  11418  climuni  11436  reccn2ap  11456  isumz  11532  geoisum1c  11663  prod1dc  11729  efltim  11841  dvdsval2  11933  dvdscmulr  11963  dvdsmulcr  11964  modmulconst  11966  dvdsadd2b  11983  dvdsexp  12003  mulmoddvds  12005  divalglemeuneg  12064  zsupssdc  12091  gcdaddm  12121  dvdsgcdb  12150  mulgcd  12153  gcddiv  12156  uzwodc  12174  lcmdvdsb  12222  mulgcddvds  12232  qredeq  12234  divgcdcoprm0  12239  cncongr1  12241  euclemma  12284  rpexp  12291  rpexp12i  12293  fermltl  12372  prmdiv  12373  odzcllem  12380  odzdvds  12383  odzphi  12384  vfermltl  12389  coprimeprodsq  12395  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem13  12414  pceu  12433  pcdvdsb  12458  pcgcd1  12466  dvdsprmpweq  12473  sumhashdc  12485  ctinf  12587  fvsetsid  12652  ressressg  12693  ressabsg  12694  rngplusgg  12754  imasaddvallemg  12898  qusaddvallemg  12916  plusfvalg  12946  mgmb1mgm1  12951  issubmnd  13023  ress0g  13024  gsumfzz  13067  grpasscan2  13136  grpidrcan  13137  grpidlcan  13138  grpinvadd  13150  grpsubeq0  13158  grppncan  13163  dfgrp3mlem  13170  dfgrp3me  13172  grpsubpropd2  13177  imasgrp2  13180  imasgrp  13181  mhmmnd  13186  mulgnn0p1  13203  mulgnnsubcl  13204  mulgnn0subcl  13205  mulgsubcl  13206  mulgneg  13210  mulgaddcom  13216  mulginvcom  13217  submmulg  13236  subgcl  13254  subgsubcl  13255  subgsub  13256  subgmulg  13258  nsgconj  13276  nsgid  13285  quseccl0g  13301  ghmmulg  13326  ghmeqker  13341  f1ghm0to0  13342  kerf1ghm  13344  ablinvadd  13380  ablsub4  13383  ablpncan2  13386  subgabl  13402  gsumfzconst  13411  rngcl  13440  imasrng  13452  srgcl  13466  ringcl  13509  crngcom  13510  ringidss  13525  ringcom  13527  imasring  13560  opprringbg  13576  unitmulcl  13609  unitmulclb  13610  dvrcl  13631  unitdvcl  13632  dvrcan1  13636  dvrcan3  13637  rhmmul  13660  subrngrng  13698  subrngmcl  13705  subrgmcl  13729  subrgdv  13734  rrgeq0  13761  domneq0  13768  islmod  13787  scafvalg  13803  lmodcom  13829  rmodislmodlem  13846  rmodislmod  13847  lssclg  13860  lssvnegcl  13872  lssintclm  13880  lspss  13895  lspun  13898  lspsnvsi  13914  rspssp  13990  rnglidlmmgm  13992  rnglidlmsgrp  13993  rnglidlrng  13994  zndvds  14137  2basgeng  14250  iuncld  14283  ntrss  14287  restco  14342  restabs  14343  cnprcl2k  14374  lmconst  14384  cnrest2  14404  cnmpt2t  14461  psmetsym  14497  psmetge0  14499  xmetge0  14533  xmetsym  14536  blvalps  14556  blval  14557  xblcntrps  14581  xblcntr  14582  xmssym  14637  blsscls2  14661  bdxmet  14669  txmetcnp  14686  dvfvalap  14835  dvid  14847  dvcnp2cntop  14848  elplyr  14886  rpcxpadd  15040  rpcxpsub  15043  rpmulcxp  15044  rpdivcxp  15046  cxpmul  15047  rpcxple2  15052  rpcxplt2  15053  rplogbval  15077  rplogbcl  15078  rplogbreexp  15085  relogbexpap  15090  logbleb  15093  logblt  15094  rplogbcxp  15095  rpcxplogb  15096  relogbcxpbap  15097  lgsneg1  15141  lgsmod  15142  lgsne0  15154  lgssq  15156  lgsdirnn0  15163  lgsdinn0  15164  findset  15437