Theorem 3anidm23 1423

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  supsn  9363  infsn  9397  grusn  10698  subeq0  11390  halfaddsub  12357  avglt2  12363  modabs2  13809  efsub  16009  sinmul  16081  divalgmod  16317  modgcd  16443  pythagtriplem4  16731  pythagtriplem16  16742  pltirr  18239  latjidm  18368  latmidm  18380  ipopos  18442  mulgmodid  18992  f1omvdcnv  19323  lsmss1  19544  rhmsubclem3  20572  zntoslem  21463  obsipid  21629  smadiadetlem2  22549  smadiadet  22555  ordtt1  23264  xmet0  24228  nmsq  25092  tcphcphlem3  25131  tcphcph  25135  grpoidinvlem1  30448  grpodivid  30486  nvmid  30603  ipidsq  30654  5oalem1  31598  3oalem2  31607  unopf1o  31860  unopnorm  31861  hmopre  31867  ballotlemfc0  34467  ballotlemfcc  34468  gcdabsorb  35733  cgr3rflx  36038  endofsegid  36069  tailini  36360  nnssi2  36439  nndivlub  36442  brin2  38396  opoccl  39183  opococ  39184  opexmid  39196  opnoncon  39197  cmtidN  39246  ltrniotaidvalN  40572  pell14qrexpclnn0  42849  rmxdbl  42922  rmydbl  42923  rhmsubcALTVlem3  48277