Theorem 3anidm23 1424

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  supsn  9380  infsn  9414  grusn  10719  subeq0  11411  halfaddsub  12378  avglt2  12384  modabs2  13829  efsub  16029  sinmul  16101  divalgmod  16337  modgcd  16463  pythagtriplem4  16751  pythagtriplem16  16762  pltirr  18260  latjidm  18389  latmidm  18401  ipopos  18463  mulgmodid  19047  f1omvdcnv  19377  lsmss1  19598  rhmsubclem3  20624  zntoslem  21515  obsipid  21681  smadiadetlem2  22612  smadiadet  22618  ordtt1  23327  xmet0  24290  nmsq  25154  tcphcphlem3  25193  tcphcph  25197  grpoidinvlem1  30583  grpodivid  30621  nvmid  30738  ipidsq  30789  5oalem1  31733  3oalem2  31742  unopf1o  31995  unopnorm  31996  hmopre  32002  ballotlemfc0  34652  ballotlemfcc  34653  gcdabsorb  35946  cgr3rflx  36250  endofsegid  36281  tailini  36572  nnssi2  36651  nndivlub  36654  brin2  38641  opoccl  39522  opococ  39523  opexmid  39535  opnoncon  39536  cmtidN  39585  ltrniotaidvalN  40911  pell14qrexpclnn0  43175  rmxdbl  43248  rmydbl  43249  rhmsubcALTVlem3  48596