Theorem 3anidm12 1331

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

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

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 1006

This theorem is referenced by:  3anidm13  1332  syl2an3an  1334  fovcl  6130  prarloclemarch2  7642  nq02m  7688  recexprlem1ssl  7856  recexprlem1ssu  7857  nncan  8411  dividap  8884  modqid0  10616  sqdividap  10870  subsq  10912  retanclap  12304  tannegap  12310  gcd0id  12571  coprm  12737