Theorem 3anidm23 1423

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

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

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

This theorem is referenced by:  supsn  9512  infsn  9545  grusn  10844  subeq0  11535  halfaddsub  12499  avglt2  12505  modabs2  13945  efsub  16136  sinmul  16208  divalgmod  16443  modgcd  16569  pythagtriplem4  16857  pythagtriplem16  16868  pltirr  18380  latjidm  18507  latmidm  18519  ipopos  18581  mulgmodid  19131  f1omvdcnv  19462  lsmss1  19683  rhmsubclem3  20687  zntoslem  21575  obsipid  21742  smadiadetlem2  22670  smadiadet  22676  ordtt1  23387  xmet0  24352  nmsq  25228  tcphcphlem3  25267  tcphcph  25271  grpoidinvlem1  30523  grpodivid  30561  nvmid  30678  ipidsq  30729  5oalem1  31673  3oalem2  31682  unopf1o  31935  unopnorm  31936  hmopre  31942  ballotlemfc0  34495  ballotlemfcc  34496  gcdabsorb  35750  cgr3rflx  36055  endofsegid  36086  tailini  36377  nnssi2  36456  nndivlub  36459  brin2  38410  opoccl  39195  opococ  39196  opexmid  39208  opnoncon  39209  cmtidN  39258  ltrniotaidvalN  40585  pell14qrexpclnn0  42877  rmxdbl  42951  rmydbl  42952  rhmsubcALTVlem3  48199