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

Theorem 3anidm13 1242
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 1159 . 2  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
323anidm12 1241 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  npncan2  9328  ltsubpos  9520  subge02  9543  halfaddsub  10201  avglt1  10205  hashssdif  11677  pythagtriplem4  13193  pythagtriplem14  13202  lsmss2  15300  grpoidinvlem2  21793  hvpncan3  22544  bcm1n  24151  sltasym  25627  leaddle0  28093  3anidm12p1  28918  3impcombi  28929
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