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

Theorem 3simpa 985
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 967 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 460 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  3simpb  986  3simpc  987  simp1  988  simp2  989  3adant3  1008  3adantl3  1146  3adantr3  1149  funtpg  5568  ftpg  5993  ovig  6314  undifixp  7401  tz9.1c  8053  ackbij1lem16  8507  enqeq  9206  prlem934  9305  lt2halves  10662  nn0n0n1ge2  10746  ixxssixx  11417  ltdifltdiv  11781  hash2prd  12285  hashtpg  12290  2swrdeqwrdeq  12451  swrd0swrd0  12461  swrdccatid  12492  dvdscmulr  13665  dvdsmulcr  13666  dvds2add  13668  dvds2sub  13669  dvdstr  13670  vdwlem12  14157  cshwsidrepswmod0  14225  cshwshashlem2  14227  lmhmlem  17218  psgndiflemA  18142  mpt2frlmd  18313  matsc  18454  mdetdiaglem  18522  2ndcctbss  19177  dvfsumrlim  21621  dvfsumrlim2  21622  ulmval  21963  axcontlem2  23348  cusgra2v  23507  2mwlk  23564  constr3lem4  23670  constr3trllem2  23674  constr3trllem3  23675  ismndo1  23968  leopmul  25675  strlem3a  25793  0elsiga  26693  afsval  27131  cgr3permute3  28214  cgr3com  28220  colineardim1  28228  brofs2  28244  brifs2  28245  btwnconn1lem4  28257  btwnconn1lem5  28258  btwnconn1lem6  28259  midofsegid  28271  ftc1anclem8  28614  sdclem2  28778  iocinico  29727  sigaras  30031  sigarms  30032  pr1eqbg  30261  otel3xp  30268  wlkelwrd  30420  wlkiswwlk2  30471  wwlknimpb  30478  clwwisshclww  30611  frg2woteq  30793  numclwwlk5  30845  gsumlsscl  30960  ldepspr  31116  lincresunit3lem3  31117  lincresunit3lem1  31122  lincresunit3  31124  m2cnstpminv  31216  pmatcollpw1id  31228  pmatcollpw1dstlem1  31229  pmatcollpwfsupp  31231  pmatcollpw1lem4  31232  pmatcollpw1lem5  31233  pmatcollpwlem  31235  pmattomply1ghmlem1  31255  pmattomply1ghmlem2  31256  pmattomply1rn  31259  mp2pm2mplem4  31266  mp2pm2mplem5  31267  mp2pm2mp  31268  chfacfisf  31310  chfacfisfcpmat  31311  cpmidgsumm2pm  31325  cpmidpmat  31329  cpmadumatpoly  31340  bnj999  32252  lsmcv2  32982  lvolnleat  33535  paddasslem14  33785  4atexlemswapqr  34015  isltrn2N  34072  cdlemftr1  34519  cdlemg5  34557
  Copyright terms: Public domain W3C validator