Theorem 3anidm23 1448

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  supsn  9446  infsn  9480  grusn  10816  subeq0  11511  halfaddsub  12504  avglt2  12510  modabs2  13968  efsub  16192  sinmul  16264  divalgmod  16500  modgcd  16626  pythagtriplem4  16915  pythagtriplem16  16926  pltirr  18425  latjidm  18554  latmidm  18566  ipopos  18628  mulgmodid  19237  f1omvdcnv  19572  lsmss1  19793  rhmsubclem3  20850  zntoslem  21770  obsipid  21936  smadiadetlem2  22887  smadiadet  22893  ordtt1  23605  xmet0  24569  nmsq  25423  tcphcphlem3  25462  tcphcph  25466  grpoidinvlem1  30971  grpodivid  31009  nvmid  31126  ipidsq  31177  5oalem1  32121  3oalem2  32130  unopf1o  32383  unopnorm  32384  hmopre  32390  ballotlemfc0  34991  ballotlemfcc  34992  gcdabsorb  36316  cgr3rflx  36621  endofsegid  36652  tailini  36982  nnssi2  37061  nndivlub  37064  brin2  39173  opoccl  40054  opococ  40055  opexmid  40067  opnoncon  40068  cmtidN  40117  ltrniotaidvalN  41443  pell14qrexpclnn0  43694  rmxdbl  43767  rmydbl  43768  rhmsubcALTVlem3  49185