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

Theorem 3simpa 952
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 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 446 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3simpb  953  3simpc  954  simp1  955  simp2  956  3adant3  975  3adantl3  1113  3adantr3  1116  ovig  5969  undifixp  6852  tz9.1c  7412  ackbij1lem16  7861  enqeq  8558  prlem934  8657  lt2halves  9946  ixxssixx  10670  dvdscmulr  12557  dvdsmulcr  12558  dvds2add  12560  dvds2sub  12561  dvdstr  12562  vdwlem12  13039  lmhmlem  15786  2ndcctbss  17181  dvfsumrlim  19378  dvfsumrlim2  19379  ulmval  19759  ismndo1  21011  leopmul  22714  strlem3a  22832  axcontlem2  24004  cgr3permute3  24081  cgr3com  24087  colineardim1  24095  brofs2  24111  brifs2  24112  btwnconn1lem4  24124  btwnconn1lem5  24125  btwnconn1lem6  24126  midofsegid  24138  definc  24691  grpodlcan  24788  limptlimpr2lem1  24986  islimrs3  24993  islimrs4  24994  cmpassoh  25213  cmpmon  25227  icmpmon  25228  tartarmap  25300  isrocatset  25369  cmp2morp  25370  sdclem2  25864  fnchoice  27112  stoweidlem10  27171  stoweidlem22  27183  stoweidlem34  27195  sigaras  27257  sigarms  27258  bnj999  28362  lsmcv2  28592  lvolnleat  29145  paddasslem14  29395  4atexlemswapqr  29625  isltrn2N  29682  cdlemftr1  30129  cdlemg5  30167
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator