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  9424  infsn  9458  grusn  10757  subeq0  11448  halfaddsub  12415  avglt2  12421  modabs2  13867  efsub  16068  sinmul  16140  divalgmod  16376  modgcd  16502  pythagtriplem4  16790  pythagtriplem16  16801  pltirr  18294  latjidm  18421  latmidm  18433  ipopos  18495  mulgmodid  19045  f1omvdcnv  19374  lsmss1  19595  rhmsubclem3  20596  zntoslem  21466  obsipid  21631  smadiadetlem2  22551  smadiadet  22557  ordtt1  23266  xmet0  24230  nmsq  25094  tcphcphlem3  25133  tcphcph  25137  grpoidinvlem1  30433  grpodivid  30471  nvmid  30588  ipidsq  30639  5oalem1  31583  3oalem2  31592  unopf1o  31845  unopnorm  31846  hmopre  31852  ballotlemfc0  34484  ballotlemfcc  34485  gcdabsorb  35737  cgr3rflx  36042  endofsegid  36073  tailini  36364  nnssi2  36443  nndivlub  36446  brin2  38400  opoccl  39187  opococ  39188  opexmid  39200  opnoncon  39201  cmtidN  39250  ltrniotaidvalN  40577  pell14qrexpclnn0  42854  rmxdbl  42928  rmydbl  42929  rhmsubcALTVlem3  48271