Theorem 3anidm23 1419

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  supsn  9192  infsn  9225  grusn  10544  subeq0  11230  halfaddsub  12189  avglt2  12195  modabs2  13606  efsub  15790  sinmul  15862  divalgmod  16096  modgcd  16221  prmdvdssqOLD  16405  pythagtriplem4  16501  pythagtriplem16  16512  pltirr  18034  latjidm  18161  latmidm  18173  ipopos  18235  mulgmodid  18723  f1omvdcnv  19033  lsmss1  19252  zntoslem  20745  obsipid  20910  smadiadetlem2  21794  smadiadet  21800  ordtt1  22511  xmet0  23476  nmsq  24339  tcphcphlem3  24378  tcphcph  24382  grpoidinvlem1  28845  grpodivid  28883  nvmid  29000  ipidsq  29051  5oalem1  29995  3oalem2  30004  unopf1o  30257  unopnorm  30258  hmopre  30264  ballotlemfc0  32438  ballotlemfcc  32439  gcdabsorb  33695  cgr3rflx  34335  endofsegid  34366  tailini  34544  nnssi2  34623  nndivlub  34626  brin2  36514  opoccl  37187  opococ  37188  opexmid  37200  opnoncon  37201  cmtidN  37250  ltrniotaidvalN  38576  pell14qrexpclnn0  40668  rmxdbl  40741  rmydbl  40742  rhmsubclem3  45598  rhmsubcALTVlem3  45616