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

Theorem 3simpa 954
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 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 447 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3simpb  955  3simpc  956  simp1  957  simp2  958  3adant3  977  3adantl3  1115  3adantr3  1118  funtpg  5493  ftpg  5908  ovig  6187  undifixp  7090  tz9.1c  7658  ackbij1lem16  8107  enqeq  8803  prlem934  8902  lt2halves  10194  nn0n0n1ge2  10272  ixxssixx  10922  hashtpg  11683  dvdscmulr  12870  dvdsmulcr  12871  dvds2add  12873  dvds2sub  12874  dvdstr  12875  vdwlem12  13352  lmhmlem  16097  2ndcctbss  17510  dvfsumrlim  19907  dvfsumrlim2  19908  ulmval  20288  cusgra2v  21463  2mwlk  21520  constr3lem4  21626  constr3trllem2  21630  constr3trllem3  21631  ismndo1  21924  leopmul  23629  strlem3a  23747  0elsiga  24489  axcontlem2  25896  cgr3permute3  25973  cgr3com  25979  colineardim1  25987  brofs2  26003  brifs2  26004  btwnconn1lem4  26016  btwnconn1lem5  26017  btwnconn1lem6  26018  midofsegid  26030  sdclem2  26427  sigaras  27802  sigarms  27803  pr1eqbg  28036  otel3xp  28042  ltdifltdiv  28116  swrd0swrd0  28158  2cshwmod  28213  cshwssizelem4a  28236  frg2woteq  28376  bnj999  29255  lsmcv2  29754  lvolnleat  30307  paddasslem14  30557  4atexlemswapqr  30787  isltrn2N  30844  cdlemftr1  31291  cdlemg5  31329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator