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

Theorem 3simpa 988
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 970 . 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 968
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 970
This theorem is referenced by:  3simpb  989  3simpc  990  simp1  991  simp2  992  3adant3  1011  3adantl3  1149  3adantr3  1152  otel3xp  5029  funtpg  5631  ftpg  6064  ovig  6401  undifixp  7497  tz9.1c  8152  ackbij1lem16  8606  enqeq  9303  prlem934  9402  lt2halves  10764  nn0n0n1ge2  10850  ixxssixx  11534  ltdifltdiv  11924  hash2prd  12473  hashtpg  12478  2swrdeqwrdeq  12630  swrd0swrd0  12640  swrdccatid  12674  dvdscmulr  13864  dvdsmulcr  13865  dvds2add  13867  dvds2sub  13868  dvdstr  13869  vdwlem12  14360  cshwsidrepswmod0  14428  cshwshashlem2  14430  lmhmlem  17453  psgndiflemA  18399  mpt2frlmd  18570  matsc  18714  scmatrhmcl  18792  mdetdiaglem  18862  decpmatid  19033  decpmatmullem  19034  mp2pm2mplem4  19072  chfacfisf  19117  chfacfisfcpmat  19118  cpmidgsumm2pm  19132  cpmidpmat  19136  cpmadumatpoly  19146  2ndcctbss  19717  dvfsumrlim  22162  dvfsumrlim2  22163  ulmval  22504  axcontlem2  23939  cusgra2v  24126  2mwlk  24185  wlkelwrd  24194  constr3lem4  24311  constr3trllem2  24315  constr3trllem3  24316  wlkiswwlk2  24361  wwlknimpb  24368  clwwisshclww  24471  frg2woteq  24725  numclwwlk5  24777  ismndo1  25010  leopmul  26717  strlem3a  26835  0elsiga  27742  afsval  28179  cgr3permute3  29262  cgr3com  29268  colineardim1  29276  brofs2  29292  brifs2  29293  btwnconn1lem4  29305  btwnconn1lem5  29306  btwnconn1lem6  29307  midofsegid  29319  ftc1anclem8  29663  sdclem2  29827  iocinico  30775  eliccre  31061  sigaras  31496  sigarms  31497  pr1eqbg  31721  gsumlsscl  31926  ldepspr  32024  lincresunit3lem3  32025  lincresunit3lem1  32030  lincresunit3  32032  bnj999  32971  lsmcv2  33703  lvolnleat  34256  paddasslem14  34506  4atexlemswapqr  34736  isltrn2N  34793  cdlemftr1  35240  cdlemg5  35278
  Copyright terms: Public domain W3C validator