Theorem 3anidm12 1332

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 1233	. 2 |- ( ph -> ( ( ph /\ ps ) -> ch ) )
3	2	anabsi5 581	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3anidm13  1333  syl2an3an  1335  fovcl  6137  prarloclemarch2  7699  nq02m  7745  recexprlem1ssl  7913  recexprlem1ssu  7914  nncan  8467  dividap  8940  modqid0  10675  sqdividap  10929  subsq  10971  retanclap  12363  tannegap  12369  gcd0id  12630  coprm  12796