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

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

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 1088

This theorem is referenced by:  supsn  9374  infsn  9408  grusn  10713  subeq0  11405  halfaddsub  12372  avglt2  12378  modabs2  13823  efsub  16023  sinmul  16095  divalgmod  16331  modgcd  16457  pythagtriplem4  16745  pythagtriplem16  16756  pltirr  18254  latjidm  18383  latmidm  18395  ipopos  18457  mulgmodid  19041  f1omvdcnv  19371  lsmss1  19592  rhmsubclem3  20618  zntoslem  21509  obsipid  21675  smadiadetlem2  22606  smadiadet  22612  ordtt1  23321  xmet0  24284  nmsq  25148  tcphcphlem3  25187  tcphcph  25191  grpoidinvlem1  30528  grpodivid  30566  nvmid  30683  ipidsq  30734  5oalem1  31678  3oalem2  31687  unopf1o  31940  unopnorm  31941  hmopre  31947  ballotlemfc0  34599  ballotlemfcc  34600  gcdabsorb  35893  cgr3rflx  36197  endofsegid  36228  tailini  36519  nnssi2  36598  nndivlub  36601  brin2  38562  opoccl  39393  opococ  39394  opexmid  39406  opnoncon  39407  cmtidN  39456  ltrniotaidvalN  40782  pell14qrexpclnn0  43050  rmxdbl  43123  rmydbl  43124  rhmsubcALTVlem3  48471