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

Theorem 3simpa 1011
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 993 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 466 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  3simpb  1012  3simpc  1013  simp1  1014  simp2  1015  3adant3  1034  3adantl3  1172  3adantr3  1175  otel3xp  4889  funtpg  5651  ftpg  6098  ovig  6445  el2xptp0  6864  wfrlem17  7078  undifixp  7584  tz9.1c  8240  ackbij1lem16  8691  enqeq  9385  prlem934  9484  lt2halves  10876  nn0n0n1ge2  10961  ixxssixx  11678  ltdifltdiv  12098  hash2prd  12667  hashtpg  12674  2swrdeqwrdeq  12846  swrd0swrd0  12856  swrdccatid  12890  sumtp  13859  dvdscmulr  14380  dvdsmulcr  14381  dvds2add  14383  dvds2sub  14384  dvdstr  14386  vdwlem12  14991  cshwsidrepswmod0  15114  cshwshashlem2  15116  initoeu2lem0  15957  estrreslem1  16071  funcestrcsetclem9  16082  funcsetcestrclem9  16097  sgrp2nmndlem4  16711  lmhmlem  18301  psgndiflemA  19218  mpt2frlmd  19384  matsc  19524  scmatrhmcl  19602  mdetdiaglem  19672  decpmatid  19843  decpmatmullem  19844  mp2pm2mplem4  19882  chfacfisf  19927  chfacfisfcpmat  19928  cpmidgsumm2pm  19942  cpmidpmat  19946  cpmadumatpoly  19956  2ndcctbss  20519  dvfsumrlim  23032  dvfsumrlim2  23033  ulmval  23384  relogbmul  23763  axcontlem2  25044  cusgra2v  25239  2mwlk  25298  wlkelwrd  25307  constr3lem4  25424  constr3trllem2  25428  constr3trllem3  25429  wlkiswwlk2  25474  wwlknimpb  25481  clwwisshclww  25584  frg2woteq  25837  numclwwlk5  25889  ismndo1  26121  leopmul  27836  strlem3a  27954  0elsiga  28985  afsval  29537  bnj999  29817  cgr3permute3  30863  cgr3com  30869  colineardim1  30877  brofs2  30893  brifs2  30894  btwnconn1lem4  30906  btwnconn1lem5  30907  btwnconn1lem6  30908  midofsegid  30920  isbasisrelowllem1  31803  isbasisrelowllem2  31804  icoreclin  31805  ftc1anclem8  32069  sdclem2  32116  lsmcv2  32640  lvolnleat  33193  paddasslem14  33443  4atexlemswapqr  33673  isltrn2N  33730  cdlemftr1  34179  cdlemg5  34217  iocinico  36141  pwinfi2  36211  relexpxpnnidm  36340  sigaras  38502  sigarms  38503  bgoldbtbndlem4  38941  bgoldbtbnd  38942  pfxsuffeqwrdeq  38987  pfxccatpfx1  39008  pfxccatpfx2  39009  pr1eqbg  39031  funvtxval  39166  structvtxval  39169  structiedg0val  39170  uspgr1v1eop  39374  uhgrissubgr  39397  subgrprop3  39398  0uhgrsubgr  39401  2m1wlk  39681  1wlkelwrd  39694  uhgr1wlkspth  39787  usgr2wlkspth  39791  2pthon3v-av  39892  uhgr3cyclex  39923  umgr3v3e3cycl  39925  mhmismgmhm  40079  funcringcsetcALTV2lem9  40319  funcringcsetclem9ALTV  40342  gsumlsscl  40441  ldepspr  40539  lincresunit3lem3  40540  lincresunit3lem1  40545  lincresunit3  40547
  Copyright terms: Public domain W3C validator