Theorem 3anidm23 1424

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 1119	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒)
3	2	anabss3 676	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  9383  infsn  9417  grusn  10724  subeq0  11417  halfaddsub  12407  avglt2  12413  modabs2  13861  efsub  16064  sinmul  16136  divalgmod  16372  modgcd  16498  pythagtriplem4  16787  pythagtriplem16  16798  pltirr  18296  latjidm  18425  latmidm  18437  ipopos  18499  mulgmodid  19086  f1omvdcnv  19416  lsmss1  19637  rhmsubclem3  20661  zntoslem  21552  obsipid  21718  smadiadetlem2  22645  smadiadet  22651  ordtt1  23360  xmet0  24323  nmsq  25177  tcphcphlem3  25216  tcphcph  25220  grpoidinvlem1  30596  grpodivid  30634  nvmid  30751  ipidsq  30802  5oalem1  31746  3oalem2  31755  unopf1o  32008  unopnorm  32009  hmopre  32015  ballotlemfc0  34659  ballotlemfcc  34660  gcdabsorb  35954  cgr3rflx  36258  endofsegid  36289  tailini  36580  nnssi2  36659  nndivlub  36662  brin2  38781  opoccl  39662  opococ  39663  opexmid  39675  opnoncon  39676  cmtidN  39725  ltrniotaidvalN  41051  pell14qrexpclnn0  43320  rmxdbl  43393  rmydbl  43394  rhmsubcALTVlem3  48779