Theorem 3anidm23 1432

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  supsn  9405  infsn  9439  grusn  10748  subeq0  11443  halfaddsub  12440  avglt2  12446  modabs2  13901  efsub  16104  sinmul  16176  divalgmod  16412  modgcd  16538  pythagtriplem4  16827  pythagtriplem16  16838  pltirr  18337  latjidm  18466  latmidm  18478  ipopos  18540  mulgmodid  19127  f1omvdcnv  19456  lsmss1  19677  rhmsubclem3  20705  zntoslem  21577  obsipid  21743  smadiadetlem2  22693  smadiadet  22699  ordtt1  23408  xmet0  24371  nmsq  25225  tcphcphlem3  25264  tcphcph  25268  grpoidinvlem1  30642  grpodivid  30680  nvmid  30797  ipidsq  30848  5oalem1  31792  3oalem2  31801  unopf1o  32054  unopnorm  32055  hmopre  32061  ballotlemfc0  34734  ballotlemfcc  34735  gcdabsorb  36038  cgr3rflx  36342  endofsegid  36373  tailini  36674  nnssi2  36753  nndivlub  36756  brin2  38875  opoccl  39756  opococ  39757  opexmid  39769  opnoncon  39770  cmtidN  39819  ltrniotaidvalN  41145  pell14qrexpclnn0  43381  rmxdbl  43454  rmydbl  43455  rhmsubcALTVlem3  48843