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  5468  ftpg  5883  ovig  6162  undifixp  7065  tz9.1c  7630  ackbij1lem16  8079  enqeq  8775  prlem934  8874  lt2halves  10166  nn0n0n1ge2  10244  ixxssixx  10894  hashtpg  11654  dvdscmulr  12841  dvdsmulcr  12842  dvds2add  12844  dvds2sub  12845  dvdstr  12846  vdwlem12  13323  lmhmlem  16068  2ndcctbss  17479  dvfsumrlim  19876  dvfsumrlim2  19877  ulmval  20257  cusgra2v  21432  2mwlk  21489  constr3lem4  21595  constr3trllem2  21599  constr3trllem3  21600  ismndo1  21893  leopmul  23598  strlem3a  23716  0elsiga  24458  axcontlem2  25816  cgr3permute3  25893  cgr3com  25899  colineardim1  25907  brofs2  25923  brifs2  25924  btwnconn1lem4  25936  btwnconn1lem5  25937  btwnconn1lem6  25938  midofsegid  25950  sdclem2  26344  sigaras  27720  sigarms  27721  pr1eqbg  27952  otel3xp  27958  swrd0swrd0  28022  frg2woteq  28171  bnj999  29046  lsmcv2  29524  lvolnleat  30077  paddasslem14  30327  4atexlemswapqr  30557  isltrn2N  30614  cdlemftr1  31061  cdlemg5  31099
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