Theorem 3anidm23 1446

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  supsn  9432  infsn  9466  grusn  10788  subeq0  11483  halfaddsub  12476  avglt2  12482  modabs2  13937  efsub  16155  sinmul  16227  divalgmod  16463  modgcd  16589  pythagtriplem4  16878  pythagtriplem16  16889  pltirr  18388  latjidm  18517  latmidm  18529  ipopos  18591  mulgmodid  19178  f1omvdcnv  19513  lsmss1  19734  rhmsubclem3  20771  zntoslem  21685  obsipid  21851  smadiadetlem2  22800  smadiadet  22806  ordtt1  23515  xmet0  24478  nmsq  25332  tcphcphlem3  25371  tcphcph  25375  grpoidinvlem1  30822  grpodivid  30860  nvmid  30977  ipidsq  31028  5oalem1  31972  3oalem2  31981  unopf1o  32234  unopnorm  32235  hmopre  32241  ballotlemfc0  34849  ballotlemfcc  34850  gcdabsorb  36196  cgr3rflx  36500  endofsegid  36531  tailini  36831  nnssi2  36910  nndivlub  36913  brin2  39033  opoccl  39914  opococ  39915  opexmid  39927  opnoncon  39928  cmtidN  39977  ltrniotaidvalN  41303  pell14qrexpclnn0  43541  rmxdbl  43614  rmydbl  43615  rhmsubcALTVlem3  48993