Theorem 3anidm12 1383

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

Step	Hyp	Ref	Expression
1		3anidm12.1	. . 3 |- ( ( ph /\ ph /\ ps ) -> ch )
2	1	3expib 1268	. 2 |- ( ph -> ( ( ph /\ ps ) -> ch ) )
3	2	anabsi5 858	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anidm13  1384  syl2an3an  1386  dedth3v  4144  nncan  10310  divid  10714  sqdivid  12929  subsq  12972  o1lo1  14268  retancl  14872  tanneg  14878  gcd0id  15240  coprm  15423  ablonncan  27411  kbpj  28815  xdivid  29636  xrsmulgzz  29678  expgrowthi  38532  dvconstbi  38533  3ornot23  38715  3anidm12p2  39034  sinhpcosh  42481  reseccl  42494  recsccl  42495  recotcl  42496  onetansqsecsq  42502