Theorem 3anidm23 1421

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 1118	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒)
3	2	anabss3 674	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  supsn  9541  infsn  9574  grusn  10873  subeq0  11562  halfaddsub  12526  avglt2  12532  modabs2  13956  efsub  16148  sinmul  16220  divalgmod  16454  modgcd  16579  pythagtriplem4  16866  pythagtriplem16  16877  pltirr  18405  latjidm  18532  latmidm  18544  ipopos  18606  mulgmodid  19153  f1omvdcnv  19486  lsmss1  19707  rhmsubclem3  20709  zntoslem  21598  obsipid  21765  smadiadetlem2  22691  smadiadet  22697  ordtt1  23408  xmet0  24373  nmsq  25247  tcphcphlem3  25286  tcphcph  25290  grpoidinvlem1  30536  grpodivid  30574  nvmid  30691  ipidsq  30742  5oalem1  31686  3oalem2  31695  unopf1o  31948  unopnorm  31949  hmopre  31955  ballotlemfc0  34457  ballotlemfcc  34458  gcdabsorb  35712  cgr3rflx  36018  endofsegid  36049  tailini  36342  nnssi2  36421  nndivlub  36424  brin2  38365  opoccl  39150  opococ  39151  opexmid  39163  opnoncon  39164  cmtidN  39213  ltrniotaidvalN  40540  pell14qrexpclnn0  42822  rmxdbl  42896  rmydbl  42897  rhmsubcALTVlem3  48006