Theorem 3anidm23 1417

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

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

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 1085

This theorem is referenced by:  supsn  8922  infsn  8955  grusn  10212  subeq0  10898  halfaddsub  11857  avglt2  11863  modabs2  13263  efsub  15438  sinmul  15510  divalgmod  15740  modgcd  15863  pythagtriplem4  16139  pythagtriplem16  16150  pltirr  17556  latjidm  17667  latmidm  17679  ipopos  17753  mulgmodid  18249  f1omvdcnv  18555  lsmss1  18774  zntoslem  20686  obsipid  20849  smadiadetlem2  21256  smadiadet  21262  ordtt1  21970  xmet0  22935  nmsq  23781  tcphcphlem3  23819  tcphcph  23823  grpoidinvlem1  28265  grpodivid  28303  nvmid  28420  ipidsq  28471  5oalem1  29415  3oalem2  29424  unopf1o  29677  unopnorm  29678  hmopre  29684  ballotlemfc0  31757  ballotlemfcc  31758  pdivsq  32988  gcdabsorb  32991  cgr3rflx  33522  endofsegid  33553  tailini  33731  nnssi2  33810  nndivlub  33813  brin2  35689  opoccl  36362  opococ  36363  opexmid  36375  opnoncon  36376  cmtidN  36425  ltrniotaidvalN  37751  pell14qrexpclnn0  39555  rmxdbl  39628  rmydbl  39629  rhmsubclem3  44444  rhmsubcALTVlem3  44462