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  4487  tfisi  4681  sotri2  5130  sotri3  5131  feq123  5469  sefvex  5654  fvmptt  5732  fnfvima  5882  cocan1  5921  cocan2  5922  ovexg  6045  ovmpox  6143  ovmpoga  6144  fvmpopr2d  6151  caovimo  6209  tfr1onlembxssdm  6502  tfr1onlembfn  6503  tfrcllembxssdm  6515  tfrcllembfn  6516  freccllem  6561  frecfcllem  6563  frecsuclem  6565  frecrdg  6567  domssr  6944  mapxpen  7027  dif1en  7059  diffifi  7074  unsnfidcex  7103  unfidisj  7105  undifdc  7107  resfnfinfinss  7127  funrnfi  7130  sbthlemi9  7153  elfir  7161  difinfsn  7288  ctssdc  7301  djuassen  7420  xpdjuen  7421  mulcanenq  7593  ltanqg  7608  mulcanenq0ec  7653  addnnnq0  7657  distrprg  7796  aptipr  7849  addsrpr  7953  mulsrpr  7954  mulasssrg  7966  ltpsrprg  8011  axmulass  8081  axpre-ltadd  8094  subadd2  8371  nppcan  8389  nppcan3  8391  subsub2  8395  subsub4  8400  npncan3  8405  pnpcan  8406  pnncan  8408  subcan  8422  ltadd1  8597  leadd1  8598  leadd2  8599  ltsubadd  8600  ltsubadd2  8601  lesubadd  8602  lesubadd2  8603  ltaddsub  8604  leaddsub  8606  lesub1  8624  lesub2  8625  ltsub1  8626  ltsub2  8627  gt0add  8741  apreap  8755  lemul1  8761  reapmul1lem  8762  reapmul1  8763  reapadd1  8764  remulext1  8767  remulext2  8768  apadd2  8777  mulext2  8781  mulap0r  8783  leltap  8793  ltap  8801  apsub1  8810  recexaplem2  8820  mulcanap  8833  mulcanap2  8834  divvalap  8842  divmulap  8843  divcanap1  8849  diveqap0  8850  divap0b  8851  divrecap  8856  divassap  8858  div23ap  8859  divdirap  8865  divcanap3  8866  div11ap  8868  diveqap1  8873  divmuldivap  8880  divcanap5  8882  redivclap  8899  div2negap  8903  apmul1  8956  apmul2  8957  div2subap  9005  ltdiv1  9036  ledivmul  9045  lemuldiv  9049  lt2msq1  9053  ltdiv23  9060  squeeze0  9072  ofnegsub  9130  zaddcllemneg  9506  eluzsub  9774  nn01to3  9839  rpgecl  9905  addlelt  9991  xleadd1  10098  xltadd1  10099  lbioog  10136  ubioc1  10152  ubicc2  10208  icoshftf1o  10214  fzen  10266  nelfzo  10375  ubmelfzo  10433  ssfzo12  10457  ubmelm1fzo  10459  fzosplitprm1  10468  zsupssdc  10486  rebtwn2zlemshrink  10501  qbtwnre  10504  icogelb  10513  flqwordi  10536  flqword2  10537  flltdivnn0lt  10552  modqcl  10576  mulqmod0  10580  modqmulnn  10592  modqabs2  10608  modqmuladdnn0  10618  qnegmod  10619  addmodid  10622  modqm1p1mod0  10625  modifeq2int  10636  modqdi  10642  modqeqmodmin  10644  modfzo0difsn  10645  frec2uzf1od  10656  exp3val  10791  expnegap0  10797  expgt1  10827  exprecap  10830  expmulzap  10835  leexp2a  10842  expubnd  10846  mulbinom2  10906  bernneq2  10911  expnbnd  10913  fihashss  11067  fihashssdif  11069  fimaxq  11078  ccatval2  11162  ccatass  11172  ccatw2s1leng  11202  ccat2s1fvwd  11211  swrdval  11216  swrdnd  11227  pfxfv  11252  pfxpfx  11276  ccats1pfxeq  11282  ccats1pfxeqrex  11283  s3cl  11354  s3fv0g  11359  s3fv1g  11360  s3fv2g  11361  shftuz  11365  shftfibg  11368  cjdivap  11457  resqrtcl  11577  absdivap  11618  abssubne0  11639  maxleast  11761  lemininf  11782  ltmininf  11783  xrmaxltsup  11806  xrmaxaddlem  11808  xrmaxadd  11809  xrmineqinf  11817  xrltmininf  11818  xrminltinf  11820  xrminadd  11823  climuni  11841  reccn2ap  11861  isumz  11937  geoisum1c  12068  prod1dc  12134  efltim  12246  dvdsval2  12338  dvdscmulr  12368  dvdsmulcr  12369  modmulconst  12371  dvdsadd2b  12388  dvdsexp  12409  mulmoddvds  12411  divalglemeuneg  12471  gcdaddm  12542  dvdsgcdb  12571  mulgcd  12574  gcddiv  12577  uzwodc  12595  lcmdvdsb  12643  mulgcddvds  12653  qredeq  12655  divgcdcoprm0  12660  cncongr1  12662  euclemma  12705  rpexp  12712  rpexp12i  12714  fermltl  12793  prmdiv  12794  odzcllem  12802  odzdvds  12805  odzphi  12806  vfermltl  12811  coprimeprodsq  12817  pythagtriplem6  12830  pythagtriplem7  12831  pythagtriplem12  12835  pythagtriplem13  12836  pceu  12855  pcdvdsb  12880  pcgcd1  12888  dvdsprmpweq  12895  sumhashdc  12907  ctinf  13038  fvsetsid  13103  ressressg  13145  ressabsg  13146  rngplusgg  13207  imasaddvallemg  13385  qusaddvallemg  13403  plusfvalg  13433  mgmb1mgm1  13438  issubmnd  13512  ress0g  13513  imasmnd2  13522  imasmnd  13523  gsumfzz  13565  grpasscan2  13634  grpidrcan  13635  grpidlcan  13636  grpinvadd  13648  grpsubeq0  13656  grppncan  13661  dfgrp3mlem  13668  dfgrp3me  13670  grpsubpropd2  13675  pwsinvg  13682  imasgrp2  13684  imasgrp  13685  mhmmnd  13690  mulgnn0p1  13707  mulgnnsubcl  13708  mulgnn0subcl  13709  mulgsubcl  13710  mulgneg  13714  mulgaddcom  13720  mulginvcom  13721  submmulg  13740  subgcl  13758  subgsubcl  13759  subgsub  13760  subgmulg  13762  nsgconj  13780  nsgid  13789  quseccl0g  13805  ghmmulg  13830  ghmeqker  13845  f1ghm0to0  13846  kerf1ghm  13848  ablinvadd  13884  ablsub4  13887  ablpncan2  13890  subgabl  13906  gsumfzconst  13915  rngcl  13944  imasrng  13956  srgcl  13970  ringcl  14013  crngcom  14014  ringidss  14029  ringcom  14031  imasring  14064  opprringbg  14080  unitmulcl  14114  unitmulclb  14115  dvrcl  14136  unitdvcl  14137  dvrcan1  14141  dvrcan3  14142  rhmmul  14165  subrngrng  14203  subrngmcl  14210  subrgmcl  14234  subrgdv  14239  rrgeq0  14266  domneq0  14273  islmod  14292  scafvalg  14308  lmodcom  14334  rmodislmodlem  14351  rmodislmod  14352  lssclg  14365  lssvnegcl  14377  lssintclm  14385  lspss  14400  lspun  14403  lspsnvsi  14419  rspssp  14495  rnglidlmmgm  14497  rnglidlmsgrp  14498  rnglidlrng  14499  zndvds  14650  2basgeng  14793  iuncld  14826  ntrss  14830  restco  14885  restabs  14886  cnprcl2k  14917  lmconst  14927  cnrest2  14947  cnmpt2t  15004  psmetsym  15040  psmetge0  15042  xmetge0  15076  xmetsym  15079  blvalps  15099  blval  15100  xblcntrps  15124  xblcntr  15125  xmssym  15180  blsscls2  15204  bdxmet  15212  txmetcnp  15229  dvfvalap  15392  dvid  15406  dvidre  15408  dvcnp2cntop  15410  elplyr  15451  rpcxpadd  15616  rpcxpsub  15619  rpmulcxp  15620  rpdivcxp  15622  cxpmul  15623  rpcxple2  15629  rpcxplt2  15630  rplogbval  15656  rplogbcl  15657  rplogbreexp  15664  relogbexpap  15669  logbleb  15672  logblt  15673  rplogbcxp  15674  rpcxplogb  15675  relogbcxpbap  15676  sgmppw  15703  lgsneg1  15741  lgsmod  15742  lgsne0  15754  lgssq  15756  lgsdirnn0  15763  lgsdinn0  15764  lgsquad  15796  funvtxvalg  15874  funiedgvalg  15875  lpvtx  15916  ausgrumgrien  16005  ausgrusgrien  16006  wlkl1loop  16146  clwwlknonex2  16224  findset  16450