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

Theorem 3anidm13 1277
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 1194 . 2  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
323anidm12 1276 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  npncan2  9739  ltsubpos  9934  leaddle0  9957  subge02  9958  halfaddsub  10661  avglt1  10665  hashssdif  12271  pythagtriplem4  13990  pythagtriplem14  13999  lsmss2  16271  grpoidinvlem2  23829  hvpncan3  24581  bcm1n  26215  sltasym  27949  3anidm12p1  31841  3impcombi  31852
  Copyright terms: Public domain W3C validator