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

Theorem 3anidm13 1287
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 1203 . 2  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
323anidm12 1286 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  npncan2  9851  ltsubpos  10050  leaddle0  10073  subge02  10074  halfaddsub  10778  avglt1  10782  hashssdif  12454  pythagtriplem4  14220  pythagtriplem14  14229  lsmss2  16560  grpoidinvlem2  25079  hvpncan3  25831  bcm1n  27472  sltasym  29407  3anidm12p1  33336  3impcombi  33347
  Copyright terms: Public domain W3C validator