Theorem 3anidm23 1420

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  supsn  9220  infsn  9253  grusn  10549  subeq0  11236  halfaddsub  12195  avglt2  12201  modabs2  13614  efsub  15798  sinmul  15870  divalgmod  16104  modgcd  16229  prmdvdssqOLD  16413  pythagtriplem4  16509  pythagtriplem16  16520  pltirr  18042  latjidm  18169  latmidm  18181  ipopos  18243  mulgmodid  18731  f1omvdcnv  19041  lsmss1  19260  zntoslem  20753  obsipid  20918  smadiadetlem2  21802  smadiadet  21808  ordtt1  22519  xmet0  23484  nmsq  24347  tcphcphlem3  24386  tcphcph  24390  grpoidinvlem1  28853  grpodivid  28891  nvmid  29008  ipidsq  29059  5oalem1  30003  3oalem2  30012  unopf1o  30265  unopnorm  30266  hmopre  30272  ballotlemfc0  32446  ballotlemfcc  32447  gcdabsorb  33703  cgr3rflx  34343  endofsegid  34374  tailini  34552  nnssi2  34631  nndivlub  34634  brin2  36522  opoccl  37195  opococ  37196  opexmid  37208  opnoncon  37209  cmtidN  37258  ltrniotaidvalN  38584  pell14qrexpclnn0  40675  rmxdbl  40748  rmydbl  40749  rhmsubclem3  45603  rhmsubcALTVlem3  45621