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  9485  infsn  9519  grusn  10818  subeq0  11509  halfaddsub  12474  avglt2  12480  modabs2  13922  efsub  16118  sinmul  16190  divalgmod  16425  modgcd  16551  pythagtriplem4  16839  pythagtriplem16  16850  pltirr  18345  latjidm  18472  latmidm  18484  ipopos  18546  mulgmodid  19096  f1omvdcnv  19425  lsmss1  19646  rhmsubclem3  20647  zntoslem  21517  obsipid  21682  smadiadetlem2  22602  smadiadet  22608  ordtt1  23317  xmet0  24281  nmsq  25146  tcphcphlem3  25185  tcphcph  25189  grpoidinvlem1  30485  grpodivid  30523  nvmid  30640  ipidsq  30691  5oalem1  31635  3oalem2  31644  unopf1o  31897  unopnorm  31898  hmopre  31904  ballotlemfc0  34525  ballotlemfcc  34526  gcdabsorb  35767  cgr3rflx  36072  endofsegid  36103  tailini  36394  nnssi2  36473  nndivlub  36476  brin2  38427  opoccl  39212  opococ  39213  opexmid  39225  opnoncon  39226  cmtidN  39275  ltrniotaidvalN  40602  pell14qrexpclnn0  42889  rmxdbl  42963  rmydbl  42964  rhmsubcALTVlem3  48258