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

Theorem 3simpa 993
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3simpa

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 975 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3simpb  994  3simpc  995  simp1  996  simp2  997  3adant3  1016  3adantl3  1154  3adantr3  1157  otel3xp  5040  funtpg  5643  ftpg  6081  ovig  6424  el2xptp0  6844  undifixp  7525  tz9.1c  8182  ackbij1lem16  8636  enqeq  9333  prlem934  9432  lt2halves  10798  nn0n0n1ge2  10884  ixxssixx  11572  ltdifltdiv  11966  hash2prd  12518  hashtpg  12523  2swrdeqwrdeq  12678  swrd0swrd0  12688  swrdccatid  12722  dvdscmulr  14012  dvdsmulcr  14013  dvds2add  14015  dvds2sub  14016  dvdstr  14018  vdwlem12  14510  cshwsidrepswmod0  14579  cshwshashlem2  14581  sgrp2nmndlem4  16046  lmhmlem  17675  psgndiflemA  18637  mpt2frlmd  18808  matsc  18952  scmatrhmcl  19030  mdetdiaglem  19100  decpmatid  19271  decpmatmullem  19272  mp2pm2mplem4  19310  chfacfisf  19355  chfacfisfcpmat  19356  cpmidgsumm2pm  19370  cpmidpmat  19374  cpmadumatpoly  19384  2ndcctbss  19956  dvfsumrlim  22432  dvfsumrlim2  22433  ulmval  22775  axcontlem2  24268  cusgra2v  24462  2mwlk  24521  wlkelwrd  24530  constr3lem4  24647  constr3trllem2  24651  constr3trllem3  24652  wlkiswwlk2  24697  wwlknimpb  24704  clwwisshclww  24807  frg2woteq  25060  numclwwlk5  25112  ismndo1  25346  leopmul  27053  strlem3a  27171  0elsiga  28114  afsval  28551  cgr3permute3  29697  cgr3com  29703  colineardim1  29711  brofs2  29727  brifs2  29728  btwnconn1lem4  29740  btwnconn1lem5  29741  btwnconn1lem6  29742  midofsegid  29754  ftc1anclem8  30097  sdclem2  30235  iocinico  31179  sigaras  32072  sigarms  32073  pr1eqbg  32297  mhmismgmhm  32494  initoeu2lem0  32619  estrreslem1  32643  funcestrcsetclem9  32654  funcsetcestrclem9  32669  funcringcsetcOLD2lem9  32852  funcringcsetclem9OLD  32875  gsumlsscl  32976  ldepspr  33074  lincresunit3lem3  33075  lincresunit3lem1  33080  lincresunit3  33082  bnj999  34015  lsmcv2  34754  lvolnleat  35307  paddasslem14  35557  4atexlemswapqr  35787  isltrn2N  35844  cdlemftr1  36293  cdlemg5  36331  pwinfi2  37747
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 975
  Copyright terms: Public domain W3C validator