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  9375  infsn  9409  grusn  10716  subeq0  11409  halfaddsub  12399  avglt2  12405  modabs2  13853  efsub  16056  sinmul  16128  divalgmod  16364  modgcd  16490  pythagtriplem4  16779  pythagtriplem16  16790  pltirr  18288  latjidm  18417  latmidm  18429  ipopos  18491  mulgmodid  19078  f1omvdcnv  19408  lsmss1  19629  rhmsubclem3  20653  zntoslem  21525  obsipid  21691  smadiadetlem2  22617  smadiadet  22623  ordtt1  23332  xmet0  24295  nmsq  25149  tcphcphlem3  25188  tcphcph  25192  grpoidinvlem1  30563  grpodivid  30601  nvmid  30718  ipidsq  30769  5oalem1  31713  3oalem2  31722  unopf1o  31975  unopnorm  31976  hmopre  31982  ballotlemfc0  34625  ballotlemfcc  34626  gcdabsorb  35920  cgr3rflx  36224  endofsegid  36255  tailini  36546  nnssi2  36625  nndivlub  36628  brin2  38747  opoccl  39628  opococ  39629  opexmid  39641  opnoncon  39642  cmtidN  39691  ltrniotaidvalN  41017  pell14qrexpclnn0  43282  rmxdbl  43355  rmydbl  43356  rhmsubcALTVlem3  48747