Theorem 3anidm23 1424

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 676	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  9390  infsn  9424  grusn  10729  subeq0  11421  halfaddsub  12388  avglt2  12394  modabs2  13839  efsub  16039  sinmul  16111  divalgmod  16347  modgcd  16473  pythagtriplem4  16761  pythagtriplem16  16772  pltirr  18270  latjidm  18399  latmidm  18411  ipopos  18473  mulgmodid  19060  f1omvdcnv  19390  lsmss1  19611  rhmsubclem3  20637  zntoslem  21528  obsipid  21694  smadiadetlem2  22625  smadiadet  22631  ordtt1  23340  xmet0  24303  nmsq  25167  tcphcphlem3  25206  tcphcph  25210  grpoidinvlem1  30598  grpodivid  30636  nvmid  30753  ipidsq  30804  5oalem1  31748  3oalem2  31757  unopf1o  32010  unopnorm  32011  hmopre  32017  ballotlemfc0  34677  ballotlemfcc  34678  gcdabsorb  35972  cgr3rflx  36276  endofsegid  36307  tailini  36598  nnssi2  36677  nndivlub  36680  brin2  38718  opoccl  39599  opococ  39600  opexmid  39612  opnoncon  39613  cmtidN  39662  ltrniotaidvalN  40988  pell14qrexpclnn0  43252  rmxdbl  43325  rmydbl  43326  rhmsubcALTVlem3  48672