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  9431  infsn  9465  grusn  10764  subeq0  11455  halfaddsub  12422  avglt2  12428  modabs2  13874  efsub  16075  sinmul  16147  divalgmod  16383  modgcd  16509  pythagtriplem4  16797  pythagtriplem16  16808  pltirr  18301  latjidm  18428  latmidm  18440  ipopos  18502  mulgmodid  19052  f1omvdcnv  19381  lsmss1  19602  rhmsubclem3  20603  zntoslem  21473  obsipid  21638  smadiadetlem2  22558  smadiadet  22564  ordtt1  23273  xmet0  24237  nmsq  25101  tcphcphlem3  25140  tcphcph  25144  grpoidinvlem1  30440  grpodivid  30478  nvmid  30595  ipidsq  30646  5oalem1  31590  3oalem2  31599  unopf1o  31852  unopnorm  31853  hmopre  31859  ballotlemfc0  34491  ballotlemfcc  34492  gcdabsorb  35744  cgr3rflx  36049  endofsegid  36080  tailini  36371  nnssi2  36450  nndivlub  36453  brin2  38407  opoccl  39194  opococ  39195  opexmid  39207  opnoncon  39208  cmtidN  39257  ltrniotaidvalN  40584  pell14qrexpclnn0  42861  rmxdbl  42935  rmydbl  42936  rhmsubcALTVlem3  48275