Theorem 3anidm12 1336

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anidm13  1337  syl2an3an  1339  fovcl  6194  prarloclemarch2  7787  nq02m  7833  recexprlem1ssl  8001  recexprlem1ssu  8002  nncan  8557  dividap  9034  modqid0  10802  sqdividap  11056  subsq  11098  retanclap  12508  tannegap  12514  gcd0id  12775  coprm  12942