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

Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086

This theorem is referenced by:  supsn  8920  infsn  8953  grusn  10215  subeq0  10901  halfaddsub  11858  avglt2  11864  modabs2  13268  efsub  15445  sinmul  15517  divalgmod  15747  modgcd  15870  pythagtriplem4  16146  pythagtriplem16  16157  pltirr  17565  latjidm  17676  latmidm  17688  ipopos  17762  mulgmodid  18258  f1omvdcnv  18564  lsmss1  18783  zntoslem  20248  obsipid  20411  smadiadetlem2  21269  smadiadet  21275  ordtt1  21984  xmet0  22949  nmsq  23799  tcphcphlem3  23837  tcphcph  23841  grpoidinvlem1  28287  grpodivid  28325  nvmid  28442  ipidsq  28493  5oalem1  29437  3oalem2  29446  unopf1o  29699  unopnorm  29700  hmopre  29706  ballotlemfc0  31860  ballotlemfcc  31861  pdivsq  33094  gcdabsorb  33097  cgr3rflx  33628  endofsegid  33659  tailini  33837  nnssi2  33916  nndivlub  33919  brin2  35817  opoccl  36490  opococ  36491  opexmid  36503  opnoncon  36504  cmtidN  36553  ltrniotaidvalN  37879  pell14qrexpclnn0  39807  rmxdbl  39880  rmydbl  39881  rhmsubclem3  44712  rhmsubcALTVlem3  44730