Theorem 3anidm23 1377

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  supsn  8261  infsn  8293  grusn  9505  subeq0  10186  halfaddsub  11142  avglt2  11148  modabs2  12566  efsub  14669  sinmul  14741  divalgmod  14967  divalgmodOLD  14968  modgcd  15091  pythagtriplem4  15362  pythagtriplem16  15373  pltirr  16786  latjidm  16897  latmidm  16909  ipopos  16983  mulgmodid  17404  f1omvdcnv  17687  lsmss1  17902  zntoslem  19724  obsipid  19885  smadiadetlem2  20289  smadiadet  20295  ordtt1  20993  xmet0  21957  nmsq  22802  tchcphlem3  22840  tchcph  22844  grpoidinvlem1  26742  grpodivid  26780  nvmid  26898  ipidsq  26949  5oalem1  27897  3oalem2  27906  unopf1o  28159  unopnorm  28160  hmopre  28166  ballotlemfc0  29881  ballotlemfcc  29882  pdivsq  30888  gcdabsorb  30891  fv2ndcnv  30926  cgr3rflx  31331  endofsegid  31362  tailini  31541  nnssi2  31624  nndivlub  31627  opoccl  33499  opococ  33500  opexmid  33512  opnoncon  33513  cmtidN  33562  ltrniotaidvalN  34889  pell14qrexpclnn0  36448  rmxdbl  36522  rmydbl  36523  rhmsubclem3  41880  rhmsubcALTVlem3  41899