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  5985  undifixp  6868  tz9.1c  7428  ackbij1lem16  7877  enqeq  8574  prlem934  8673  lt2halves  9962  ixxssixx  10686  dvdscmulr  12573  dvdsmulcr  12574  dvds2add  12576  dvds2sub  12577  dvdstr  12578  vdwlem12  13055  lmhmlem  15802  2ndcctbss  17197  dvfsumrlim  19394  dvfsumrlim2  19395  ulmval  19775  ismndo1  21027  leopmul  22730  strlem3a  22848  0elsiga  23490  axcontlem2  24665  cgr3permute3  24742  cgr3com  24748  colineardim1  24756  brofs2  24772  brifs2  24773  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem6  24787  midofsegid  24799  definc  25382  grpodlcan  25479  limptlimpr2lem1  25677  islimrs3  25684  islimrs4  25685  cmpassoh  25904  cmpmon  25918  icmpmon  25919  tartarmap  25991  isrocatset  26060  cmp2morp  26061  sdclem2  26555  fnchoice  27803  stoweidlem10  27862  stoweidlem22  27874  stoweidlem34  27886  sigaras  27948  sigarms  27949  hashtpg  28217  cusgra2v  28297  2mwlk  28330  constr3lem4  28393  constr3trllem3  28398  bnj999  29305  lsmcv2  29841  lvolnleat  30394  paddasslem14  30644  4atexlemswapqr  30874  isltrn2N  30931  cdlemftr1  31378  cdlemg5  31416
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