Theorem 3anidm12 1329

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

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

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 1004

This theorem is referenced by:  3anidm13  1330  syl2an3an  1332  fovcl  6110  prarloclemarch2  7606  nq02m  7652  recexprlem1ssl  7820  recexprlem1ssu  7821  nncan  8375  dividap  8848  modqid0  10572  sqdividap  10826  subsq  10868  retanclap  12233  tannegap  12239  gcd0id  12500  coprm  12666