Theorem 3anidm23 1449

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  supsn  9492  infsn  9526  grusn  10916  subeq0  11611  halfaddsub  12606  avglt2  12612  modabs2  14072  efsub  16297  sinmul  16369  divalgmod  16605  modgcd  16734  pythagtriplem4  17026  pythagtriplem16  17037  pltirr  18536  latjidm  18665  latmidm  18677  ipopos  18739  mulgmodid  19352  f1omvdcnv  19688  lsmss1  19909  rhmsubclem3  20969  zntoslem  21892  obsipid  22058  smadiadetlem2  23009  smadiadet  23015  ordtt1  23727  xmet0  24691  nmsq  25545  tcphcphlem3  25584  tcphcph  25588  grpoidinvlem1  31136  grpodivid  31174  nvmid  31291  ipidsq  31342  5oalem1  32286  3oalem2  32295  unopf1o  32548  unopnorm  32549  hmopre  32555  ballotlemfc0  35195  ballotlemfcc  35196  maxssj0  36006  gcdabsorb  36693  cgr3rflx  36997  endofsegid  37028  tailini  37342  nnssi2  37421  nndivlub  37424  brin2  39562  opoccl  40443  opococ  40444  opexmid  40456  opnoncon  40457  cmtidN  40506  ltrniotaidvalN  41832  pell14qrexpclnn0  44066  rmxdbl  44139  rmydbl  44140  rhmsubcALTVlem3  49585