Theorem 3anidm23 1421

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  supsn  9469  infsn  9502  grusn  10801  subeq0  11488  halfaddsub  12447  avglt2  12453  modabs2  13872  efsub  16045  sinmul  16117  divalgmod  16351  modgcd  16476  prmdvdssqOLD  16658  pythagtriplem4  16754  pythagtriplem16  16765  pltirr  18290  latjidm  18417  latmidm  18429  ipopos  18491  mulgmodid  18995  f1omvdcnv  19314  lsmss1  19535  zntoslem  21118  obsipid  21283  smadiadetlem2  22173  smadiadet  22179  ordtt1  22890  xmet0  23855  nmsq  24718  tcphcphlem3  24757  tcphcph  24761  grpoidinvlem1  29795  grpodivid  29833  nvmid  29950  ipidsq  30001  5oalem1  30945  3oalem2  30954  unopf1o  31207  unopnorm  31208  hmopre  31214  ballotlemfc0  33560  ballotlemfcc  33561  gcdabsorb  34789  cgr3rflx  35095  endofsegid  35126  tailini  35347  nnssi2  35426  nndivlub  35429  brin2  37365  opoccl  38150  opococ  38151  opexmid  38163  opnoncon  38164  cmtidN  38213  ltrniotaidvalN  39540  pell14qrexpclnn0  41686  rmxdbl  41760  rmydbl  41761  rhmsubclem3  47065  rhmsubcALTVlem3  47083