Theorem simp2 998

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  simpl2  1001  simpr2  1004  simp2i  1007  simp2d  1010  simp12  1028  simp22  1031  simp32  1034  syld3an3  1283  3ianorr  1309  stoic4b  1433  nlim0  4393  tfisi  4585  sotri2  5025  sotri3  5026  feq123  5356  sefvex  5535  fvmptt  5606  fnfvima  5749  cocan1  5785  cocan2  5786  ovexg  5906  ovmpox  6000  ovmpoga  6001  caovimo  6065  tfr1onlembxssdm  6341  tfr1onlembfn  6342  tfrcllembxssdm  6354  tfrcllembfn  6355  freccllem  6400  frecfcllem  6402  frecsuclem  6404  frecrdg  6406  mapxpen  6845  dif1en  6876  diffifi  6891  unsnfidcex  6916  unfidisj  6918  undifdc  6920  resfnfinfinss  6936  funrnfi  6938  sbthlemi9  6961  elfir  6969  difinfsn  7096  ctssdc  7109  djuassen  7213  xpdjuen  7214  mulcanenq  7381  ltanqg  7396  mulcanenq0ec  7441  addnnnq0  7445  distrprg  7584  aptipr  7637  addsrpr  7741  mulsrpr  7742  mulasssrg  7754  ltpsrprg  7799  axmulass  7869  axpre-ltadd  7882  subadd2  8157  nppcan  8175  nppcan3  8177  subsub2  8181  subsub4  8186  npncan3  8191  pnpcan  8192  pnncan  8194  subcan  8208  ltadd1  8382  leadd1  8383  leadd2  8384  ltsubadd  8385  ltsubadd2  8386  lesubadd  8387  lesubadd2  8388  ltaddsub  8389  leaddsub  8391  lesub1  8409  lesub2  8410  ltsub1  8411  ltsub2  8412  gt0add  8526  apreap  8540  lemul1  8546  reapmul1lem  8547  reapmul1  8548  reapadd1  8549  remulext1  8552  remulext2  8553  apadd2  8562  mulext2  8566  mulap0r  8568  leltap  8578  ltap  8586  apsub1  8595  recexaplem2  8605  mulcanap  8618  mulcanap2  8619  divvalap  8627  divmulap  8628  divcanap1  8634  diveqap0  8635  divap0b  8636  divrecap  8641  divassap  8643  div23ap  8644  divdirap  8650  divcanap3  8651  div11ap  8653  diveqap1  8658  divmuldivap  8665  divcanap5  8667  redivclap  8684  div2negap  8688  apmul1  8741  apmul2  8742  div2subap  8790  ltdiv1  8821  ledivmul  8830  lemuldiv  8834  lt2msq1  8838  ltdiv23  8845  squeeze0  8857  zaddcllemneg  9288  eluzsub  9553  nn01to3  9613  rpgecl  9678  addlelt  9764  xleadd1  9871  xltadd1  9872  lbioog  9909  ubioc1  9925  ubicc2  9981  icoshftf1o  9987  fzen  10038  ubmelfzo  10195  ssfzo12  10219  ubmelm1fzo  10221  fzosplitprm1  10229  rebtwn2zlemshrink  10249  qbtwnre  10252  icogelb  10261  flqwordi  10283  flqword2  10284  flltdivnn0lt  10299  modqcl  10321  mulqmod0  10325  modqmulnn  10337  modqabs2  10353  modqmuladdnn0  10363  qnegmod  10364  addmodid  10367  modqm1p1mod0  10370  modifeq2int  10381  modqdi  10387  modqeqmodmin  10389  modfzo0difsn  10390  frec2uzf1od  10401  exp3val  10517  expnegap0  10523  expgt1  10553  exprecap  10556  expmulzap  10561  leexp2a  10568  expubnd  10572  mulbinom2  10631  bernneq2  10636  expnbnd  10638  fihashss  10789  fihashssdif  10791  fimaxq  10800  shftuz  10819  shftfibg  10822  cjdivap  10911  resqrtcl  11031  absdivap  11072  abssubne0  11093  maxleast  11215  lemininf  11235  ltmininf  11236  xrmaxltsup  11259  xrmaxaddlem  11261  xrmaxadd  11262  xrmineqinf  11270  xrltmininf  11271  xrminltinf  11273  xrminadd  11276  climuni  11294  reccn2ap  11314  isumz  11390  geoisum1c  11521  prod1dc  11587  efltim  11699  dvdsval2  11790  dvdscmulr  11820  dvdsmulcr  11821  modmulconst  11823  dvdsadd2b  11840  dvdsexp  11859  mulmoddvds  11861  divalglemeuneg  11920  zsupssdc  11947  gcdaddm  11977  dvdsgcdb  12006  mulgcd  12009  gcddiv  12012  uzwodc  12030  lcmdvdsb  12076  mulgcddvds  12086  qredeq  12088  divgcdcoprm0  12093  cncongr1  12095  euclemma  12138  rpexp  12145  rpexp12i  12147  fermltl  12226  prmdiv  12227  odzcllem  12234  odzdvds  12237  odzphi  12238  vfermltl  12243  coprimeprodsq  12249  pythagtriplem6  12262  pythagtriplem7  12263  pythagtriplem12  12267  pythagtriplem13  12268  pceu  12287  pcdvdsb  12311  pcgcd1  12319  dvdsprmpweq  12326  sumhashdc  12337  ctinf  12423  fvsetsid  12488  ressressg  12526  ressabsg  12527  rngplusgg  12587  plusfvalg  12714  mgmb1mgm1  12719  issubmnd  12775  ress0g  12776  grpasscan2  12866  grpidrcan  12867  grpidlcan  12868  grpinvadd  12880  grpsubeq0  12888  grppncan  12893  dfgrp3mlem  12900  dfgrp3me  12902  grpsubpropd2  12907  mhmmnd  12912  mulgnn0p1  12926  mulgnnsubcl  12927  mulgnn0subcl  12928  mulgsubcl  12929  mulgneg  12933  mulgaddcom  12938  mulginvcom  12939  subgcl  12975  subgsubcl  12976  subgsub  12977  subgmulg  12979  nsgconj  12997  nsgid  13006  ablinvadd  13044  ablsub4  13047  ablpncan2  13050  srgcl  13084  ringcl  13127  crngcom  13128  ringidss  13143  ringcom  13145  opprringbg  13181  unitmulcl  13213  unitmulclb  13214  dvrcl  13235  unitdvcl  13236  dvrcan1  13240  dvrcan3  13241  subrgmcl  13292  subrgdv  13297  2basgeng  13453  iuncld  13486  ntrss  13490  restco  13545  restabs  13546  cnprcl2k  13577  lmconst  13587  cnrest2  13607  cnmpt2t  13664  psmetsym  13700  psmetge0  13702  xmetge0  13736  xmetsym  13739  blvalps  13759  blval  13760  xblcntrps  13784  xblcntr  13785  xmssym  13840  blsscls2  13864  bdxmet  13872  txmetcnp  13889  dvfvalap  14021  dvid  14033  dvcnp2cntop  14034  rpcxpadd  14197  rpcxpsub  14200  rpmulcxp  14201  rpdivcxp  14203  cxpmul  14204  rpcxple2  14209  rpcxplt2  14210  rplogbval  14234  rplogbcl  14235  rplogbreexp  14242  relogbexpap  14247  logbleb  14250  logblt  14251  rplogbcxp  14252  rpcxplogb  14253  relogbcxpbap  14254  lgsneg1  14297  lgsmod  14298  lgsne0  14310  lgssq  14312  lgsdirnn0  14319  lgsdinn0  14320  findset  14557