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

Theorem 3anidm13 1286
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 1202 . 2  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
323anidm12 1285 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  npncan2  9842  ltsubpos  10040  leaddle0  10063  subge02  10064  halfaddsub  10768  avglt1  10772  hashssdif  12436  pythagtriplem4  14198  pythagtriplem14  14207  lsmss2  16482  grpoidinvlem2  24883  hvpncan3  25635  bcm1n  27268  sltasym  29009  3anidm12p1  32683  3impcombi  32694
  Copyright terms: Public domain W3C validator