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  5501  ftpg  5916  ovig  6195  undifixp  7098  tz9.1c  7666  ackbij1lem16  8115  enqeq  8811  prlem934  8910  lt2halves  10202  nn0n0n1ge2  10280  ixxssixx  10930  hashtpg  11691  dvdscmulr  12878  dvdsmulcr  12879  dvds2add  12881  dvds2sub  12882  dvdstr  12883  vdwlem12  13360  lmhmlem  16105  2ndcctbss  17518  dvfsumrlim  19915  dvfsumrlim2  19916  ulmval  20296  cusgra2v  21471  2mwlk  21528  constr3lem4  21634  constr3trllem2  21638  constr3trllem3  21639  ismndo1  21932  leopmul  23637  strlem3a  23755  0elsiga  24497  axcontlem2  25904  cgr3permute3  25981  cgr3com  25987  colineardim1  25995  brofs2  26011  brifs2  26012  btwnconn1lem4  26024  btwnconn1lem5  26025  btwnconn1lem6  26026  midofsegid  26038  ftc1anclem8  26287  sdclem2  26446  sigaras  27821  sigarms  27822  pr1eqbg  28056  otel3xp  28062  ltdifltdiv  28148  swrd0swrd0  28202  2cshwmod  28257  cshwssizelem4a  28283  wlkelwrd  28295  frg2woteq  28449  bnj999  29328  lsmcv2  29827  lvolnleat  30380  paddasslem14  30630  4atexlemswapqr  30860  isltrn2N  30917  cdlemftr1  31364  cdlemg5  31402
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