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  4484  tfisi  4678  sotri2  5125  sotri3  5126  feq123  5464  sefvex  5647  fvmptt  5725  fnfvima  5873  cocan1  5910  cocan2  5911  ovexg  6034  ovmpox  6132  ovmpoga  6133  fvmpopr2d  6140  caovimo  6198  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfrcllembxssdm  6500  tfrcllembfn  6501  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecrdg  6552  domssr  6927  mapxpen  7005  dif1en  7037  diffifi  7052  unsnfidcex  7078  unfidisj  7080  undifdc  7082  resfnfinfinss  7102  funrnfi  7105  sbthlemi9  7128  elfir  7136  difinfsn  7263  ctssdc  7276  djuassen  7395  xpdjuen  7396  mulcanenq  7568  ltanqg  7583  mulcanenq0ec  7628  addnnnq0  7632  distrprg  7771  aptipr  7824  addsrpr  7928  mulsrpr  7929  mulasssrg  7941  ltpsrprg  7986  axmulass  8056  axpre-ltadd  8069  subadd2  8346  nppcan  8364  nppcan3  8366  subsub2  8370  subsub4  8375  npncan3  8380  pnpcan  8381  pnncan  8383  subcan  8397  ltadd1  8572  leadd1  8573  leadd2  8574  ltsubadd  8575  ltsubadd2  8576  lesubadd  8577  lesubadd2  8578  ltaddsub  8579  leaddsub  8581  lesub1  8599  lesub2  8600  ltsub1  8601  ltsub2  8602  gt0add  8716  apreap  8730  lemul1  8736  reapmul1lem  8737  reapmul1  8738  reapadd1  8739  remulext1  8742  remulext2  8743  apadd2  8752  mulext2  8756  mulap0r  8758  leltap  8768  ltap  8776  apsub1  8785  recexaplem2  8795  mulcanap  8808  mulcanap2  8809  divvalap  8817  divmulap  8818  divcanap1  8824  diveqap0  8825  divap0b  8826  divrecap  8831  divassap  8833  div23ap  8834  divdirap  8840  divcanap3  8841  div11ap  8843  diveqap1  8848  divmuldivap  8855  divcanap5  8857  redivclap  8874  div2negap  8878  apmul1  8931  apmul2  8932  div2subap  8980  ltdiv1  9011  ledivmul  9020  lemuldiv  9024  lt2msq1  9028  ltdiv23  9035  squeeze0  9047  ofnegsub  9105  zaddcllemneg  9481  eluzsub  9748  nn01to3  9808  rpgecl  9874  addlelt  9960  xleadd1  10067  xltadd1  10068  lbioog  10105  ubioc1  10121  ubicc2  10177  icoshftf1o  10183  fzen  10235  nelfzo  10344  ubmelfzo  10401  ssfzo12  10425  ubmelm1fzo  10427  fzosplitprm1  10435  zsupssdc  10453  rebtwn2zlemshrink  10468  qbtwnre  10471  icogelb  10480  flqwordi  10503  flqword2  10504  flltdivnn0lt  10519  modqcl  10543  mulqmod0  10547  modqmulnn  10559  modqabs2  10575  modqmuladdnn0  10585  qnegmod  10586  addmodid  10589  modqm1p1mod0  10592  modifeq2int  10603  modqdi  10609  modqeqmodmin  10611  modfzo0difsn  10612  frec2uzf1od  10623  exp3val  10758  expnegap0  10764  expgt1  10794  exprecap  10797  expmulzap  10802  leexp2a  10809  expubnd  10813  mulbinom2  10873  bernneq2  10878  expnbnd  10880  fihashss  11033  fihashssdif  11035  fimaxq  11044  ccatval2  11128  ccatass  11138  swrdval  11175  swrdnd  11186  pfxfv  11211  pfxpfx  11235  ccats1pfxeq  11241  ccats1pfxeqrex  11242  s3cl  11313  s3fv0g  11318  s3fv1g  11319  shftuz  11323  shftfibg  11326  cjdivap  11415  resqrtcl  11535  absdivap  11576  abssubne0  11597  maxleast  11719  lemininf  11740  ltmininf  11741  xrmaxltsup  11764  xrmaxaddlem  11766  xrmaxadd  11767  xrmineqinf  11775  xrltmininf  11776  xrminltinf  11778  xrminadd  11781  climuni  11799  reccn2ap  11819  isumz  11895  geoisum1c  12026  prod1dc  12092  efltim  12204  dvdsval2  12296  dvdscmulr  12326  dvdsmulcr  12327  modmulconst  12329  dvdsadd2b  12346  dvdsexp  12367  mulmoddvds  12369  divalglemeuneg  12429  gcdaddm  12500  dvdsgcdb  12529  mulgcd  12532  gcddiv  12535  uzwodc  12553  lcmdvdsb  12601  mulgcddvds  12611  qredeq  12613  divgcdcoprm0  12618  cncongr1  12620  euclemma  12663  rpexp  12670  rpexp12i  12672  fermltl  12751  prmdiv  12752  odzcllem  12760  odzdvds  12763  odzphi  12764  vfermltl  12769  coprimeprodsq  12775  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem13  12794  pceu  12813  pcdvdsb  12838  pcgcd1  12846  dvdsprmpweq  12853  sumhashdc  12865  ctinf  12996  fvsetsid  13061  ressressg  13103  ressabsg  13104  rngplusgg  13165  imasaddvallemg  13343  qusaddvallemg  13361  plusfvalg  13391  mgmb1mgm1  13396  issubmnd  13470  ress0g  13471  imasmnd2  13480  imasmnd  13481  gsumfzz  13523  grpasscan2  13592  grpidrcan  13593  grpidlcan  13594  grpinvadd  13606  grpsubeq0  13614  grppncan  13619  dfgrp3mlem  13626  dfgrp3me  13628  grpsubpropd2  13633  pwsinvg  13640  imasgrp2  13642  imasgrp  13643  mhmmnd  13648  mulgnn0p1  13665  mulgnnsubcl  13666  mulgnn0subcl  13667  mulgsubcl  13668  mulgneg  13672  mulgaddcom  13678  mulginvcom  13679  submmulg  13698  subgcl  13716  subgsubcl  13717  subgsub  13718  subgmulg  13720  nsgconj  13738  nsgid  13747  quseccl0g  13763  ghmmulg  13788  ghmeqker  13803  f1ghm0to0  13804  kerf1ghm  13806  ablinvadd  13842  ablsub4  13845  ablpncan2  13848  subgabl  13864  gsumfzconst  13873  rngcl  13902  imasrng  13914  srgcl  13928  ringcl  13971  crngcom  13972  ringidss  13987  ringcom  13989  imasring  14022  opprringbg  14038  unitmulcl  14071  unitmulclb  14072  dvrcl  14093  unitdvcl  14094  dvrcan1  14098  dvrcan3  14099  rhmmul  14122  subrngrng  14160  subrngmcl  14167  subrgmcl  14191  subrgdv  14196  rrgeq0  14223  domneq0  14230  islmod  14249  scafvalg  14265  lmodcom  14291  rmodislmodlem  14308  rmodislmod  14309  lssclg  14322  lssvnegcl  14334  lssintclm  14342  lspss  14357  lspun  14360  lspsnvsi  14376  rspssp  14452  rnglidlmmgm  14454  rnglidlmsgrp  14455  rnglidlrng  14456  zndvds  14607  2basgeng  14750  iuncld  14783  ntrss  14787  restco  14842  restabs  14843  cnprcl2k  14874  lmconst  14884  cnrest2  14904  cnmpt2t  14961  psmetsym  14997  psmetge0  14999  xmetge0  15033  xmetsym  15036  blvalps  15056  blval  15057  xblcntrps  15081  xblcntr  15082  xmssym  15137  blsscls2  15161  bdxmet  15169  txmetcnp  15186  dvfvalap  15349  dvid  15363  dvidre  15365  dvcnp2cntop  15367  elplyr  15408  rpcxpadd  15573  rpcxpsub  15576  rpmulcxp  15577  rpdivcxp  15579  cxpmul  15580  rpcxple2  15586  rpcxplt2  15587  rplogbval  15613  rplogbcl  15614  rplogbreexp  15621  relogbexpap  15626  logbleb  15629  logblt  15630  rplogbcxp  15631  rpcxplogb  15632  relogbcxpbap  15633  sgmppw  15660  lgsneg1  15698  lgsmod  15699  lgsne0  15711  lgssq  15713  lgsdirnn0  15720  lgsdinn0  15721  lgsquad  15753  funvtxvalg  15831  funiedgvalg  15832  lpvtx  15873  ausgrumgrien  15962  ausgrusgrien  15963  findset  16266