Theorem 3anidm23 1418

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  supsn  9497  infsn  9530  grusn  10829  subeq0  11518  halfaddsub  12478  avglt2  12484  modabs2  13906  efsub  16080  sinmul  16152  divalgmod  16386  modgcd  16511  prmdvdssqOLD  16693  pythagtriplem4  16791  pythagtriplem16  16802  pltirr  18330  latjidm  18457  latmidm  18469  ipopos  18531  mulgmodid  19076  f1omvdcnv  19411  lsmss1  19632  rhmsubclem3  20632  zntoslem  21507  obsipid  21673  smadiadetlem2  22610  smadiadet  22616  ordtt1  23327  xmet0  24292  nmsq  25166  tcphcphlem3  25205  tcphcph  25209  grpoidinvlem1  30386  grpodivid  30424  nvmid  30541  ipidsq  30592  5oalem1  31536  3oalem2  31545  unopf1o  31798  unopnorm  31799  hmopre  31805  ballotlemfc0  34243  ballotlemfcc  34244  gcdabsorb  35475  cgr3rflx  35781  endofsegid  35812  tailini  35991  nnssi2  36070  nndivlub  36073  brin2  38011  opoccl  38796  opococ  38797  opexmid  38809  opnoncon  38810  cmtidN  38859  ltrniotaidvalN  40186  pell14qrexpclnn0  42428  rmxdbl  42502  rmydbl  42503  rhmsubcALTVlem3  47531