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

Theorem 3anidm13 1240
Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
Hypothesis
Ref Expression
3anidm13.1  |-  ( (
ph  /\  ps  /\  ph )  ->  ch )
Assertion
Ref Expression
3anidm13  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem 3anidm13
StepHypRef Expression
1 3anidm13.1 . . 3  |-  ( (
ph  /\  ps  /\  ph )  ->  ch )
213com23 1157 . 2  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
323anidm12 1239 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  npncan2  9074  ltsubpos  9266  subge02  9289  halfaddsub  9945  avglt1  9949  hashssdif  11374  pythagtriplem4  12872  pythagtriplem14  12881  lsmss2  14977  grpoidinvlem2  20872  hvpncan3  21621  bcm1n  23032  sltasym  24326  3anidm12p1  28581
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