Theorem 3anidm23 1423

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 675	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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

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 1088

This theorem is referenced by:  supsn  9400  infsn  9434  grusn  10733  subeq0  11424  halfaddsub  12391  avglt2  12397  modabs2  13843  efsub  16044  sinmul  16116  divalgmod  16352  modgcd  16478  pythagtriplem4  16766  pythagtriplem16  16777  pltirr  18274  latjidm  18403  latmidm  18415  ipopos  18477  mulgmodid  19027  f1omvdcnv  19358  lsmss1  19579  rhmsubclem3  20607  zntoslem  21498  obsipid  21664  smadiadetlem2  22584  smadiadet  22590  ordtt1  23299  xmet0  24263  nmsq  25127  tcphcphlem3  25166  tcphcph  25170  grpoidinvlem1  30483  grpodivid  30521  nvmid  30638  ipidsq  30689  5oalem1  31633  3oalem2  31642  unopf1o  31895  unopnorm  31896  hmopre  31902  ballotlemfc0  34477  ballotlemfcc  34478  gcdabsorb  35730  cgr3rflx  36035  endofsegid  36066  tailini  36357  nnssi2  36436  nndivlub  36439  brin2  38393  opoccl  39180  opococ  39181  opexmid  39193  opnoncon  39194  cmtidN  39243  ltrniotaidvalN  40570  pell14qrexpclnn0  42847  rmxdbl  42921  rmydbl  42922  rhmsubcALTVlem3  48264