Theorem 3anidm23 1422

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  supsn  9464  infsn  9497  grusn  10796  subeq0  11483  halfaddsub  12442  avglt2  12448  modabs2  13867  efsub  16040  sinmul  16112  divalgmod  16346  modgcd  16471  prmdvdssqOLD  16653  pythagtriplem4  16749  pythagtriplem16  16760  pltirr  18285  latjidm  18412  latmidm  18424  ipopos  18486  mulgmodid  18988  f1omvdcnv  19307  lsmss1  19528  zntoslem  21104  obsipid  21269  smadiadetlem2  22158  smadiadet  22164  ordtt1  22875  xmet0  23840  nmsq  24703  tcphcphlem3  24742  tcphcph  24746  grpoidinvlem1  29745  grpodivid  29783  nvmid  29900  ipidsq  29951  5oalem1  30895  3oalem2  30904  unopf1o  31157  unopnorm  31158  hmopre  31164  ballotlemfc0  33480  ballotlemfcc  33481  gcdabsorb  34709  cgr3rflx  35015  endofsegid  35046  tailini  35250  nnssi2  35329  nndivlub  35332  brin2  37268  opoccl  38053  opococ  38054  opexmid  38066  opnoncon  38067  cmtidN  38116  ltrniotaidvalN  39443  pell14qrexpclnn0  41590  rmxdbl  41664  rmydbl  41665  rhmsubclem3  46940  rhmsubcALTVlem3  46958