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

Theorem 3anidm12 1285
Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
Hypothesis
Ref Expression
3anidm12.1  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3anidm12  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem 3anidm12
StepHypRef Expression
1 3anidm12.1 . . 3  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
213expib 1199 . 2  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
32anabsi5 815 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:  3anidm13  1286  dedth3v  4002  nncan  9860  divid  10246  subsq  12255  o1lo1  13340  retancl  13755  tanneg  13761  gcd0id  14037  coprm  14117  gxid  25098  ablonncan  25119  kbpj  26698  xdivid  27448  xrsmulgzz  27490  expgrowthi  31162  dvconstbi  31163  sinhpcosh  32616  reseccl  32629  recsccl  32630  recotcl  32631  onetansqsecsq  32637  3ornot23  32758  eel112  32971  3anidm12p2  33085
  Copyright terms: Public domain W3C validator