Theorem simp2 1022

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simpl2  1025  simpr2  1028  simp2i  1031  simp2d  1034  simp12  1052  simp22  1055  simp32  1058  syld3an3  1316  3ianorr  1343  intn3an2d  1391  stoic4b  1475  nlim0  4485  tfisi  4679  sotri2  5126  sotri3  5127  feq123  5465  sefvex  5650  fvmptt  5728  fnfvima  5878  cocan1  5917  cocan2  5918  ovexg  6041  ovmpox  6139  ovmpoga  6140  fvmpopr2d  6147  caovimo  6205  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfrcllembxssdm  6508  tfrcllembfn  6509  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  domssr  6937  mapxpen  7017  dif1en  7049  diffifi  7064  unsnfidcex  7093  unfidisj  7095  undifdc  7097  resfnfinfinss  7117  funrnfi  7120  sbthlemi9  7143  elfir  7151  difinfsn  7278  ctssdc  7291  djuassen  7410  xpdjuen  7411  mulcanenq  7583  ltanqg  7598  mulcanenq0ec  7643  addnnnq0  7647  distrprg  7786  aptipr  7839  addsrpr  7943  mulsrpr  7944  mulasssrg  7956  ltpsrprg  8001  axmulass  8071  axpre-ltadd  8084  subadd2  8361  nppcan  8379  nppcan3  8381  subsub2  8385  subsub4  8390  npncan3  8395  pnpcan  8396  pnncan  8398  subcan  8412  ltadd1  8587  leadd1  8588  leadd2  8589  ltsubadd  8590  ltsubadd2  8591  lesubadd  8592  lesubadd2  8593  ltaddsub  8594  leaddsub  8596  lesub1  8614  lesub2  8615  ltsub1  8616  ltsub2  8617  gt0add  8731  apreap  8745  lemul1  8751  reapmul1lem  8752  reapmul1  8753  reapadd1  8754  remulext1  8757  remulext2  8758  apadd2  8767  mulext2  8771  mulap0r  8773  leltap  8783  ltap  8791  apsub1  8800  recexaplem2  8810  mulcanap  8823  mulcanap2  8824  divvalap  8832  divmulap  8833  divcanap1  8839  diveqap0  8840  divap0b  8841  divrecap  8846  divassap  8848  div23ap  8849  divdirap  8855  divcanap3  8856  div11ap  8858  diveqap1  8863  divmuldivap  8870  divcanap5  8872  redivclap  8889  div2negap  8893  apmul1  8946  apmul2  8947  div2subap  8995  ltdiv1  9026  ledivmul  9035  lemuldiv  9039  lt2msq1  9043  ltdiv23  9050  squeeze0  9062  ofnegsub  9120  zaddcllemneg  9496  eluzsub  9764  nn01to3  9824  rpgecl  9890  addlelt  9976  xleadd1  10083  xltadd1  10084  lbioog  10121  ubioc1  10137  ubicc2  10193  icoshftf1o  10199  fzen  10251  nelfzo  10360  ubmelfzo  10418  ssfzo12  10442  ubmelm1fzo  10444  fzosplitprm1  10452  zsupssdc  10470  rebtwn2zlemshrink  10485  qbtwnre  10488  icogelb  10497  flqwordi  10520  flqword2  10521  flltdivnn0lt  10536  modqcl  10560  mulqmod0  10564  modqmulnn  10576  modqabs2  10592  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  modqm1p1mod0  10609  modifeq2int  10620  modqdi  10626  modqeqmodmin  10628  modfzo0difsn  10629  frec2uzf1od  10640  exp3val  10775  expnegap0  10781  expgt1  10811  exprecap  10814  expmulzap  10819  leexp2a  10826  expubnd  10830  mulbinom2  10890  bernneq2  10895  expnbnd  10897  fihashss  11051  fihashssdif  11053  fimaxq  11062  ccatval2  11146  ccatass  11156  swrdval  11195  swrdnd  11206  pfxfv  11231  pfxpfx  11255  ccats1pfxeq  11261  ccats1pfxeqrex  11262  s3cl  11333  s3fv0g  11338  s3fv1g  11339  shftuz  11343  shftfibg  11346  cjdivap  11435  resqrtcl  11555  absdivap  11596  abssubne0  11617  maxleast  11739  lemininf  11760  ltmininf  11761  xrmaxltsup  11784  xrmaxaddlem  11786  xrmaxadd  11787  xrmineqinf  11795  xrltmininf  11796  xrminltinf  11798  xrminadd  11801  climuni  11819  reccn2ap  11839  isumz  11915  geoisum1c  12046  prod1dc  12112  efltim  12224  dvdsval2  12316  dvdscmulr  12346  dvdsmulcr  12347  modmulconst  12349  dvdsadd2b  12366  dvdsexp  12387  mulmoddvds  12389  divalglemeuneg  12449  gcdaddm  12520  dvdsgcdb  12549  mulgcd  12552  gcddiv  12555  uzwodc  12573  lcmdvdsb  12621  mulgcddvds  12631  qredeq  12633  divgcdcoprm0  12638  cncongr1  12640  euclemma  12683  rpexp  12690  rpexp12i  12692  fermltl  12771  prmdiv  12772  odzcllem  12780  odzdvds  12783  odzphi  12784  vfermltl  12789  coprimeprodsq  12795  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem12  12813  pythagtriplem13  12814  pceu  12833  pcdvdsb  12858  pcgcd1  12866  dvdsprmpweq  12873  sumhashdc  12885  ctinf  13016  fvsetsid  13081  ressressg  13123  ressabsg  13124  rngplusgg  13185  imasaddvallemg  13363  qusaddvallemg  13381  plusfvalg  13411  mgmb1mgm1  13416  issubmnd  13490  ress0g  13491  imasmnd2  13500  imasmnd  13501  gsumfzz  13543  grpasscan2  13612  grpidrcan  13613  grpidlcan  13614  grpinvadd  13626  grpsubeq0  13634  grppncan  13639  dfgrp3mlem  13646  dfgrp3me  13648  grpsubpropd2  13653  pwsinvg  13660  imasgrp2  13662  imasgrp  13663  mhmmnd  13668  mulgnn0p1  13685  mulgnnsubcl  13686  mulgnn0subcl  13687  mulgsubcl  13688  mulgneg  13692  mulgaddcom  13698  mulginvcom  13699  submmulg  13718  subgcl  13736  subgsubcl  13737  subgsub  13738  subgmulg  13740  nsgconj  13758  nsgid  13767  quseccl0g  13783  ghmmulg  13808  ghmeqker  13823  f1ghm0to0  13824  kerf1ghm  13826  ablinvadd  13862  ablsub4  13865  ablpncan2  13868  subgabl  13884  gsumfzconst  13893  rngcl  13922  imasrng  13934  srgcl  13948  ringcl  13991  crngcom  13992  ringidss  14007  ringcom  14009  imasring  14042  opprringbg  14058  unitmulcl  14092  unitmulclb  14093  dvrcl  14114  unitdvcl  14115  dvrcan1  14119  dvrcan3  14120  rhmmul  14143  subrngrng  14181  subrngmcl  14188  subrgmcl  14212  subrgdv  14217  rrgeq0  14244  domneq0  14251  islmod  14270  scafvalg  14286  lmodcom  14312  rmodislmodlem  14329  rmodislmod  14330  lssclg  14343  lssvnegcl  14355  lssintclm  14363  lspss  14378  lspun  14381  lspsnvsi  14397  rspssp  14473  rnglidlmmgm  14475  rnglidlmsgrp  14476  rnglidlrng  14477  zndvds  14628  2basgeng  14771  iuncld  14804  ntrss  14808  restco  14863  restabs  14864  cnprcl2k  14895  lmconst  14905  cnrest2  14925  cnmpt2t  14982  psmetsym  15018  psmetge0  15020  xmetge0  15054  xmetsym  15057  blvalps  15077  blval  15078  xblcntrps  15102  xblcntr  15103  xmssym  15158  blsscls2  15182  bdxmet  15190  txmetcnp  15207  dvfvalap  15370  dvid  15384  dvidre  15386  dvcnp2cntop  15388  elplyr  15429  rpcxpadd  15594  rpcxpsub  15597  rpmulcxp  15598  rpdivcxp  15600  cxpmul  15601  rpcxple2  15607  rpcxplt2  15608  rplogbval  15634  rplogbcl  15635  rplogbreexp  15642  relogbexpap  15647  logbleb  15650  logblt  15651  rplogbcxp  15652  rpcxplogb  15653  relogbcxpbap  15654  sgmppw  15681  lgsneg1  15719  lgsmod  15720  lgsne0  15732  lgssq  15734  lgsdirnn0  15741  lgsdinn0  15742  lgsquad  15774  funvtxvalg  15852  funiedgvalg  15853  lpvtx  15894  ausgrumgrien  15983  ausgrusgrien  15984  wlkl1loop  16099  findset  16363