Theorem 3anidm23 1545

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

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  supsn  8620  infsn  8652  grusn  9914  subeq0  10599  halfaddsub  11553  avglt2  11559  modabs2  12959  efsub  15166  sinmul  15238  divalgmod  15465  modgcd  15588  pythagtriplem4  15857  pythagtriplem16  15868  pltirr  17278  latjidm  17389  latmidm  17401  ipopos  17475  mulgmodid  17894  f1omvdcnv  18176  lsmss1  18392  zntoslem  20226  obsipid  20391  smadiadetlem2  20797  smadiadet  20803  ordtt1  21512  xmet0  22475  nmsq  23321  tcphcphlem3  23359  tcphcph  23363  grpoidinvlem1  27884  grpodivid  27922  nvmid  28039  ipidsq  28090  5oalem1  29038  3oalem2  29047  unopf1o  29300  unopnorm  29301  hmopre  29307  ballotlemfc0  31071  ballotlemfcc  31072  pdivsq  32149  gcdabsorb  32152  cgr3rflx  32674  endofsegid  32705  tailini  32883  nnssi2  32962  nndivlub  32965  brin2  34661  opoccl  35215  opococ  35216  opexmid  35228  opnoncon  35229  cmtidN  35278  ltrniotaidvalN  36604  pell14qrexpclnn0  38216  rmxdbl  38289  rmydbl  38290  rhmsubclem3  42887  rhmsubcALTVlem3  42905