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

Theorem 3anidm12 1239
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 1154 . 2  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
32anabsi5 790 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anidm13  1240  dedth3v  3611  nncan  9076  divid  9451  subsq  11210  o1lo1  12011  retancl  12422  tanneg  12428  gcd0id  12702  coprm  12779  gxid  20940  ablonncan  20961  kbpj  22536  xdivid  23111  xrsmulgzz  23307  expgrowthi  27550  dvconstbi  27551  sinhpcosh  28210  reseccl  28223  recsccl  28224  recotcl  28225  onetansqsecsq  28231  3ornot23  28270  eel112  28477  3anidm12p2  28582
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