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

Theorem 3simpa 991
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 973 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 458 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  3simpb  992  3simpc  993  simp1  994  simp2  995  3adant3  1014  3adantl3  1152  3adantr3  1155  otel3xp  4949  funtpg  5546  ftpg  5983  ovig  6323  el2xptp0  6743  undifixp  7424  tz9.1c  8074  ackbij1lem16  8528  enqeq  9223  prlem934  9322  lt2halves  10690  nn0n0n1ge2  10776  ixxssixx  11464  ltdifltdiv  11866  hash2prd  12422  hashtpg  12427  2swrdeqwrdeq  12589  swrd0swrd0  12599  swrdccatid  12633  dvdscmulr  14014  dvdsmulcr  14015  dvds2add  14017  dvds2sub  14018  dvdstr  14020  vdwlem12  14512  cshwsidrepswmod0  14581  cshwshashlem2  14583  initoeu2lem0  15409  estrreslem1  15523  funcestrcsetclem9  15534  funcsetcestrclem9  15549  sgrp2nmndlem4  16163  lmhmlem  17788  psgndiflemA  18728  mpt2frlmd  18897  matsc  19037  scmatrhmcl  19115  mdetdiaglem  19185  decpmatid  19356  decpmatmullem  19357  mp2pm2mplem4  19395  chfacfisf  19440  chfacfisfcpmat  19441  cpmidgsumm2pm  19455  cpmidpmat  19459  cpmadumatpoly  19469  2ndcctbss  20041  dvfsumrlim  22517  dvfsumrlim2  22518  ulmval  22860  relogbmul  23235  axcontlem2  24389  cusgra2v  24583  2mwlk  24642  wlkelwrd  24651  constr3lem4  24768  constr3trllem2  24772  constr3trllem3  24773  wlkiswwlk2  24818  wwlknimpb  24825  clwwisshclww  24928  frg2woteq  25181  numclwwlk5  25233  ismndo1  25463  leopmul  27169  strlem3a  27287  0elsiga  28263  afsval  28734  cgr3permute3  29850  cgr3com  29856  colineardim1  29864  brofs2  29880  brifs2  29881  btwnconn1lem4  29893  btwnconn1lem5  29894  btwnconn1lem6  29895  midofsegid  29907  ftc1anclem8  30263  sdclem2  30401  iocinico  31347  sigaras  32238  sigarms  32239  pfxsuffeqwrdeq  32581  pfxccatpfx1  32602  pfxccatpfx2  32603  pr1eqbg  32618  mhmismgmhm  32812  funcringcsetcALTV2lem9  33052  funcringcsetclem9ALTV  33075  gsumlsscl  33176  ldepspr  33274  lincresunit3lem3  33275  lincresunit3lem1  33280  lincresunit3  33282  bnj999  34362  lsmcv2  35167  lvolnleat  35720  paddasslem14  35970  4atexlemswapqr  36200  isltrn2N  36257  cdlemftr1  36706  cdlemg5  36744  pwinfi2  38176  relexpxpnnidm  38243
  Copyright terms: Public domain W3C validator