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

Theorem 3simpa 994
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 976 . 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 974
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 976
This theorem is referenced by:  3simpb  995  3simpc  996  simp1  997  simp2  998  3adant3  1017  3adantl3  1155  3adantr3  1158  otel3xp  5025  funtpg  5628  ftpg  6066  ovig  6409  el2xptp0  6829  undifixp  7507  tz9.1c  8164  ackbij1lem16  8618  enqeq  9315  prlem934  9414  lt2halves  10780  nn0n0n1ge2  10866  ixxssixx  11554  ltdifltdiv  11948  hash2prd  12500  hashtpg  12505  2swrdeqwrdeq  12660  swrd0swrd0  12670  swrdccatid  12704  dvdscmulr  13994  dvdsmulcr  13995  dvds2add  13997  dvds2sub  13998  dvdstr  14000  vdwlem12  14492  cshwsidrepswmod0  14561  cshwshashlem2  14563  sgrp2nmndlem4  16025  lmhmlem  17654  psgndiflemA  18615  mpt2frlmd  18786  matsc  18930  scmatrhmcl  19008  mdetdiaglem  19078  decpmatid  19249  decpmatmullem  19250  mp2pm2mplem4  19288  chfacfisf  19333  chfacfisfcpmat  19334  cpmidgsumm2pm  19348  cpmidpmat  19352  cpmadumatpoly  19362  2ndcctbss  19934  dvfsumrlim  22410  dvfsumrlim2  22411  ulmval  22753  axcontlem2  24246  cusgra2v  24440  2mwlk  24499  wlkelwrd  24508  constr3lem4  24625  constr3trllem2  24629  constr3trllem3  24630  wlkiswwlk2  24675  wwlknimpb  24682  clwwisshclww  24785  frg2woteq  25038  numclwwlk5  25090  ismndo1  25324  leopmul  27031  strlem3a  27149  0elsiga  28092  afsval  28529  cgr3permute3  29673  cgr3com  29679  colineardim1  29687  brofs2  29703  brifs2  29704  btwnconn1lem4  29716  btwnconn1lem5  29717  btwnconn1lem6  29718  midofsegid  29730  ftc1anclem8  30073  sdclem2  30211  iocinico  31155  sigaras  32026  sigarms  32027  pr1eqbg  32251  mhmismgmhm  32447  estrreslem1  32609  funcestrcsetclem9  32620  funcsetcestrclem9  32635  funcringcsetcOLD2lem9  32724  funcringcsetclem9OLD  32747  gsumlsscl  32846  ldepspr  32944  lincresunit3lem3  32945  lincresunit3lem1  32950  lincresunit3  32952  bnj999  33883  lsmcv2  34629  lvolnleat  35182  paddasslem14  35432  4atexlemswapqr  35662  isltrn2N  35719  cdlemftr1  36168  cdlemg5  36206  pwinfi2  37585
  Copyright terms: Public domain W3C validator