Theorem 3anidm23 1532

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

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

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  supsn  8543  infsn  8575  grusn  9818  subeq0  10499  halfaddsub  11457  avglt2  11463  modabs2  12898  efsub  15029  sinmul  15101  divalgmod  15331  divalgmodOLD  15332  modgcd  15455  pythagtriplem4  15726  pythagtriplem16  15737  pltirr  17164  latjidm  17275  latmidm  17287  ipopos  17361  mulgmodid  17782  f1omvdcnv  18064  lsmss1  18279  zntoslem  20107  obsipid  20268  smadiadetlem2  20672  smadiadet  20678  ordtt1  21385  xmet0  22348  nmsq  23194  tchcphlem3  23232  tchcph  23236  grpoidinvlem1  27667  grpodivid  27705  nvmid  27823  ipidsq  27874  5oalem1  28822  3oalem2  28831  unopf1o  29084  unopnorm  29085  hmopre  29091  ballotlemfc0  30863  ballotlemfcc  30864  pdivsq  31942  gcdabsorb  31945  cgr3rflx  32467  endofsegid  32498  tailini  32677  nnssi2  32760  nndivlub  32763  brin2  34490  opoccl  34984  opococ  34985  opexmid  34997  opnoncon  34998  cmtidN  35047  ltrniotaidvalN  36373  pell14qrexpclnn0  37932  rmxdbl  38006  rmydbl  38007  rhmsubclem3  42598  rhmsubcALTVlem3  42616