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  6161  prarloclemarch2  7736  nq02m  7782  recexprlem1ssl  7950  recexprlem1ssu  7951  nncan  8504  dividap  8977  modqid0  10716  sqdividap  10970  subsq  11012  retanclap  12412  tannegap  12418  gcd0id  12679  coprm  12845