Theorem 3anidm23 1448

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  supsn  9465  infsn  9499  grusn  10889  subeq0  11584  halfaddsub  12579  avglt2  12585  modabs2  14045  efsub  16268  sinmul  16340  divalgmod  16576  modgcd  16705  pythagtriplem4  16997  pythagtriplem16  17008  pltirr  18507  latjidm  18636  latmidm  18648  ipopos  18710  mulgmodid  19323  f1omvdcnv  19658  lsmss1  19879  rhmsubclem3  20939  zntoslem  21862  obsipid  22028  smadiadetlem2  22979  smadiadet  22985  ordtt1  23697  xmet0  24661  nmsq  25515  tcphcphlem3  25554  tcphcph  25558  grpoidinvlem1  31106  grpodivid  31144  nvmid  31261  ipidsq  31312  5oalem1  32256  3oalem2  32265  unopf1o  32518  unopnorm  32519  hmopre  32525  ballotlemfc0  35167  ballotlemfcc  35168  gcdabsorb  36557  cgr3rflx  36861  endofsegid  36892  tailini  37206  nnssi2  37285  nndivlub  37288  brin2  39413  opoccl  40294  opococ  40295  opexmid  40307  opnoncon  40308  cmtidN  40357  ltrniotaidvalN  41683  pell14qrexpclnn0  43916  rmxdbl  43989  rmydbl  43990  rhmsubcALTVlem3  49423