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

Theorem 3anidm12 1241
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 1156 . 2  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
32anabsi5 791 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3anidm13  1242  dedth3v  3785  nncan  9330  divid  9705  subsq  11488  o1lo1  12331  retancl  12743  tanneg  12749  gcd0id  13023  coprm  13100  gxid  21861  ablonncan  21882  kbpj  23459  xdivid  24174  xrsmulgzz  24200  expgrowthi  27527  dvconstbi  27528  sinhpcosh  28483  reseccl  28496  recsccl  28497  recotcl  28498  onetansqsecsq  28504  3ornot23  28591  eel112  28805  3anidm12p2  28919
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator