Theorem 3anidm23 1442

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

Hypothesis

Ref	Expression
3anidm23.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3anidm23	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem 3anidm23

Step	Hyp	Ref	Expression
1		3anidm23.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒)
2	1	3expa 1132	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒)
3	2	anabss3 685	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  supsn  9417  infsn  9451  grusn  10773  subeq0  11468  halfaddsub  12464  avglt2  12470  modabs2  13925  efsub  16142  sinmul  16214  divalgmod  16450  modgcd  16576  pythagtriplem4  16865  pythagtriplem16  16876  pltirr  18375  latjidm  18504  latmidm  18516  ipopos  18578  mulgmodid  19165  f1omvdcnv  19494  lsmss1  19715  rhmsubclem3  20747  zntoslem  21615  obsipid  21781  smadiadetlem2  22731  smadiadet  22737  ordtt1  23446  xmet0  24409  nmsq  25263  tcphcphlem3  25302  tcphcph  25306  grpoidinvlem1  30714  grpodivid  30752  nvmid  30869  ipidsq  30920  5oalem1  31864  3oalem2  31873  unopf1o  32126  unopnorm  32127  hmopre  32133  ballotlemfc0  34792  ballotlemfcc  34793  gcdabsorb  36105  cgr3rflx  36409  endofsegid  36440  tailini  36741  nnssi2  36820  nndivlub  36823  brin2  38942  opoccl  39823  opococ  39824  opexmid  39836  opnoncon  39837  cmtidN  39886  ltrniotaidvalN  41212  pell14qrexpclnn0  43448  rmxdbl  43521  rmydbl  43522  rhmsubcALTVlem3  48896