Theorem 3anidm23 1447

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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

This theorem is used by:  supsn  9431  infsn  9465  grusn  10795  subeq0  11490  halfaddsub  12483  avglt2  12489  modabs2  13945  efsub  16162  sinmul  16234  divalgmod  16470  modgcd  16596  pythagtriplem4  16885  pythagtriplem16  16896  pltirr  18395  latjidm  18524  latmidm  18536  ipopos  18598  mulgmodid  19185  f1omvdcnv  19520  lsmss1  19741  rhmsubclem3  20797  zntoslem  21717  obsipid  21883  smadiadetlem2  22832  smadiadet  22838  ordtt1  23547  xmet0  24510  nmsq  25364  tcphcphlem3  25403  tcphcph  25407  grpoidinvlem1  30867  grpodivid  30905  nvmid  31022  ipidsq  31073  5oalem1  32017  3oalem2  32026  unopf1o  32279  unopnorm  32280  hmopre  32286  ballotlemfc0  34892  ballotlemfcc  34893  gcdabsorb  36250  cgr3rflx  36554  endofsegid  36585  tailini  36915  nnssi2  36994  nndivlub  36997  brin2  39115  opoccl  39996  opococ  39997  opexmid  40009  opnoncon  40010  cmtidN  40059  ltrniotaidvalN  41385  pell14qrexpclnn0  43621  rmxdbl  43694  rmydbl  43695  rhmsubcALTVlem3  49076