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  9443  infsn  9477  grusn  10860  subeq0  11555  halfaddsub  12548  avglt2  12554  modabs2  14013  efsub  16235  sinmul  16307  divalgmod  16543  modgcd  16669  pythagtriplem4  16958  pythagtriplem16  16969  pltirr  18468  latjidm  18597  latmidm  18609  ipopos  18671  mulgmodid  19284  f1omvdcnv  19619  lsmss1  19840  rhmsubclem3  20900  zntoslem  21823  obsipid  21989  smadiadetlem2  22940  smadiadet  22946  ordtt1  23658  xmet0  24622  nmsq  25476  tcphcphlem3  25515  tcphcph  25519  grpoidinvlem1  31039  grpodivid  31077  nvmid  31194  ipidsq  31245  5oalem1  32189  3oalem2  32198  unopf1o  32451  unopnorm  32452  hmopre  32458  ballotlemfc0  35059  ballotlemfcc  35060  gcdabsorb  36436  cgr3rflx  36741  endofsegid  36772  tailini  37086  nnssi2  37165  nndivlub  37168  brin2  39290  opoccl  40171  opococ  40172  opexmid  40184  opnoncon  40185  cmtidN  40234  ltrniotaidvalN  41560  pell14qrexpclnn0  43811  rmxdbl  43884  rmydbl  43885  rhmsubcALTVlem3  49302