MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3simpa 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  5443  ftpg  5857  ovig  6136  undifixp  7036  tz9.1c  7601  ackbij1lem16  8050  enqeq  8746  prlem934  8845  lt2halves  10136  nn0n0n1ge2  10214  ixxssixx  10864  hashtpg  11620  dvdscmulr  12807  dvdsmulcr  12808  dvds2add  12810  dvds2sub  12811  dvdstr  12812  vdwlem12  13289  lmhmlem  16034  2ndcctbss  17441  dvfsumrlim  19784  dvfsumrlim2  19785  ulmval  20165  cusgra2v  21339  2mwlk  21394  constr3lem4  21484  constr3trllem2  21488  constr3trllem3  21489  ismndo1  21782  leopmul  23487  strlem3a  23605  0elsiga  24295  axcontlem2  25620  cgr3permute3  25697  cgr3com  25703  colineardim1  25711  brofs2  25727  brifs2  25728  btwnconn1lem4  25740  btwnconn1lem5  25741  btwnconn1lem6  25742  midofsegid  25754  sdclem2  26139  sigaras  27515  sigarms  27516  bnj999  28668  lsmcv2  29146  lvolnleat  29699  paddasslem14  29949  4atexlemswapqr  30179  isltrn2N  30236  cdlemftr1  30683  cdlemg5  30721
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