Theorem 3anidm23 1420

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 1117	. 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  9510  infsn  9543  grusn  10842  subeq0  11533  halfaddsub  12497  avglt2  12503  modabs2  13942  efsub  16133  sinmul  16205  divalgmod  16440  modgcd  16566  pythagtriplem4  16853  pythagtriplem16  16864  pltirr  18393  latjidm  18520  latmidm  18532  ipopos  18594  mulgmodid  19144  f1omvdcnv  19477  lsmss1  19698  rhmsubclem3  20704  zntoslem  21593  obsipid  21760  smadiadetlem2  22686  smadiadet  22692  ordtt1  23403  xmet0  24368  nmsq  25242  tcphcphlem3  25281  tcphcph  25285  grpoidinvlem1  30533  grpodivid  30571  nvmid  30688  ipidsq  30739  5oalem1  31683  3oalem2  31692  unopf1o  31945  unopnorm  31946  hmopre  31952  ballotlemfc0  34474  ballotlemfcc  34475  gcdabsorb  35730  cgr3rflx  36036  endofsegid  36067  tailini  36359  nnssi2  36438  nndivlub  36441  brin2  38391  opoccl  39176  opococ  39177  opexmid  39189  opnoncon  39190  cmtidN  39239  ltrniotaidvalN  40566  pell14qrexpclnn0  42854  rmxdbl  42928  rmydbl  42929  rhmsubcALTVlem3  48127