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  3624  nncan  9092  divid  9467  subsq  11226  o1lo1  12027  retancl  12438  tanneg  12444  gcd0id  12718  coprm  12795  gxid  20956  ablonncan  20977  kbpj  22552  xdivid  23127  xrsmulgzz  23322  expgrowthi  27653  dvconstbi  27654  sinhpcosh  28464  reseccl  28477  recsccl  28478  recotcl  28479  onetansqsecsq  28485  3ornot23  28569  eel112  28782  3anidm12p2  28896
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