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  9090  ltsubpos  9282  subge02  9305  halfaddsub  9961  avglt1  9965  hashssdif  11390  pythagtriplem4  12888  pythagtriplem14  12897  lsmss2  14993  grpoidinvlem2  20888  hvpncan3  21637  bcm1n  23048  sltasym  24397  3anidm12p1  28895  3impcombi  28906
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