Theorem 3anidm23 1422

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 674	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  supsn  9467  infsn  9500  grusn  10799  subeq0  11486  halfaddsub  12445  avglt2  12451  modabs2  13870  efsub  16043  sinmul  16115  divalgmod  16349  modgcd  16474  prmdvdssqOLD  16656  pythagtriplem4  16752  pythagtriplem16  16763  pltirr  18288  latjidm  18415  latmidm  18427  ipopos  18489  mulgmodid  18993  f1omvdcnv  19312  lsmss1  19533  zntoslem  21112  obsipid  21277  smadiadetlem2  22166  smadiadet  22172  ordtt1  22883  xmet0  23848  nmsq  24711  tcphcphlem3  24750  tcphcph  24754  grpoidinvlem1  29757  grpodivid  29795  nvmid  29912  ipidsq  29963  5oalem1  30907  3oalem2  30916  unopf1o  31169  unopnorm  31170  hmopre  31176  ballotlemfc0  33491  ballotlemfcc  33492  gcdabsorb  34720  cgr3rflx  35026  endofsegid  35057  tailini  35261  nnssi2  35340  nndivlub  35343  brin2  37279  opoccl  38064  opococ  38065  opexmid  38077  opnoncon  38078  cmtidN  38127  ltrniotaidvalN  39454  pell14qrexpclnn0  41604  rmxdbl  41678  rmydbl  41679  rhmsubclem3  46986  rhmsubcALTVlem3  47004