Theorem 3anidm23 1385

Description: Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)

Hypothesis

Ref	Expression
3anidm23.1	|- ( ( ph /\ ps /\ ps ) -> ch )

Assertion

Ref	Expression
3anidm23	|- ( ( ph /\ ps ) -> ch )

Proof of Theorem 3anidm23

Step	Hyp	Ref	Expression
1		3anidm23.1	. . 3 |- ( ( ph /\ ps /\ ps ) -> ch )
2	1	3expa 1265	. 2 |- ( ( ( ph /\ ps ) /\ ps ) -> ch )
3	2	anabss3 864	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  supsn  8378  infsn  8410  grusn  9626  subeq0  10307  halfaddsub  11265  avglt2  11271  modabs2  12704  efsub  14830  sinmul  14902  divalgmod  15129  divalgmodOLD  15130  modgcd  15253  pythagtriplem4  15524  pythagtriplem16  15535  pltirr  16963  latjidm  17074  latmidm  17086  ipopos  17160  mulgmodid  17581  f1omvdcnv  17864  lsmss1  18079  zntoslem  19905  obsipid  20066  smadiadetlem2  20470  smadiadet  20476  ordtt1  21183  xmet0  22147  nmsq  22994  tchcphlem3  23032  tchcph  23036  grpoidinvlem1  27358  grpodivid  27396  nvmid  27514  ipidsq  27565  5oalem1  28513  3oalem2  28522  unopf1o  28775  unopnorm  28776  hmopre  28782  ballotlemfc0  30554  ballotlemfcc  30555  pdivsq  31635  gcdabsorb  31638  cgr3rflx  32161  endofsegid  32192  tailini  32371  nnssi2  32454  nndivlub  32457  opoccl  34481  opococ  34482  opexmid  34494  opnoncon  34495  cmtidN  34544  ltrniotaidvalN  35871  pell14qrexpclnn0  37430  rmxdbl  37504  rmydbl  37505  rhmsubclem3  42088  rhmsubcALTVlem3  42106