MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3simpa Structured version   Unicode version

Theorem 3simpa 1003
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3simpa  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 985 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 462 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 985
This theorem is referenced by:  3simpb  1004  3simpc  1005  simp1  1006  simp2  1007  3adant3  1026  3adantl3  1164  3adantr3  1167  otel3xp  4888  funtpg  5650  ftpg  6088  ovig  6431  el2xptp0  6850  wfrlem17  7062  undifixp  7568  tz9.1c  8221  ackbij1lem16  8671  enqeq  9365  prlem934  9464  lt2halves  10853  nn0n0n1ge2  10938  ixxssixx  11655  ltdifltdiv  12071  hash2prd  12636  hashtpg  12643  2swrdeqwrdeq  12809  swrd0swrd0  12819  swrdccatid  12853  sumtp  13807  dvdscmulr  14328  dvdsmulcr  14329  dvds2add  14331  dvds2sub  14332  dvdstr  14334  vdwlem12  14939  cshwsidrepswmod0  15062  cshwshashlem2  15064  initoeu2lem0  15905  estrreslem1  16019  funcestrcsetclem9  16030  funcsetcestrclem9  16045  sgrp2nmndlem4  16659  lmhmlem  18249  psgndiflemA  19165  mpt2frlmd  19331  matsc  19471  scmatrhmcl  19549  mdetdiaglem  19619  decpmatid  19790  decpmatmullem  19791  mp2pm2mplem4  19829  chfacfisf  19874  chfacfisfcpmat  19875  cpmidgsumm2pm  19889  cpmidpmat  19893  cpmadumatpoly  19903  2ndcctbss  20466  dvfsumrlim  22979  dvfsumrlim2  22980  ulmval  23331  relogbmul  23710  axcontlem2  24991  cusgra2v  25186  2mwlk  25245  wlkelwrd  25254  constr3lem4  25371  constr3trllem2  25375  constr3trllem3  25376  wlkiswwlk2  25421  wwlknimpb  25428  clwwisshclww  25531  frg2woteq  25784  numclwwlk5  25836  ismndo1  26068  leopmul  27783  strlem3a  27901  0elsiga  28942  afsval  29494  bnj999  29774  cgr3permute3  30817  cgr3com  30823  colineardim1  30831  brofs2  30847  brifs2  30848  btwnconn1lem4  30860  btwnconn1lem5  30861  btwnconn1lem6  30862  midofsegid  30874  isbasisrelowllem1  31720  isbasisrelowllem2  31721  icoreclin  31722  ftc1anclem8  31986  sdclem2  32033  lsmcv2  32562  lvolnleat  33115  paddasslem14  33365  4atexlemswapqr  33595  isltrn2N  33652  cdlemftr1  34101  cdlemg5  34139  iocinico  36064  pwinfi2  36134  relexpxpnnidm  36203  sigaras  38225  sigarms  38226  bgoldbtbndlem4  38663  bgoldbtbnd  38664  pfxsuffeqwrdeq  38707  pfxccatpfx1  38728  pfxccatpfx2  38729  pr1eqbg  38744  funvtxval  38834  structvtxval  38837  structiedg0val  38838  mhmismgmhm  39198  funcringcsetcALTV2lem9  39438  funcringcsetclem9ALTV  39461  gsumlsscl  39562  ldepspr  39660  lincresunit3lem3  39661  lincresunit3lem1  39666  lincresunit3  39668
  Copyright terms: Public domain W3C validator