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  9357  infsn  9391  grusn  10695  subeq0  11387  halfaddsub  12354  avglt2  12360  modabs2  13809  efsub  16009  sinmul  16081  divalgmod  16317  modgcd  16443  pythagtriplem4  16731  pythagtriplem16  16742  pltirr  18239  latjidm  18368  latmidm  18380  ipopos  18442  mulgmodid  19026  f1omvdcnv  19356  lsmss1  19577  rhmsubclem3  20602  zntoslem  21493  obsipid  21659  smadiadetlem2  22579  smadiadet  22585  ordtt1  23294  xmet0  24257  nmsq  25121  tcphcphlem3  25160  tcphcph  25164  grpoidinvlem1  30484  grpodivid  30522  nvmid  30639  ipidsq  30690  5oalem1  31634  3oalem2  31643  unopf1o  31896  unopnorm  31897  hmopre  31903  ballotlemfc0  34506  ballotlemfcc  34507  gcdabsorb  35794  cgr3rflx  36098  endofsegid  36129  tailini  36420  nnssi2  36499  nndivlub  36502  brin2  38461  opoccl  39292  opococ  39293  opexmid  39305  opnoncon  39306  cmtidN  39355  ltrniotaidvalN  40681  pell14qrexpclnn0  42958  rmxdbl  43031  rmydbl  43032  rhmsubcALTVlem3  48382