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

This theorem is referenced by:  supsn  9275  infsn  9308  grusn  10606  subeq0  11293  halfaddsub  12252  avglt2  12258  modabs2  13671  efsub  15854  sinmul  15926  divalgmod  16160  modgcd  16285  prmdvdssqOLD  16469  pythagtriplem4  16565  pythagtriplem16  16576  pltirr  18098  latjidm  18225  latmidm  18237  ipopos  18299  mulgmodid  18787  f1omvdcnv  19097  lsmss1  19316  zntoslem  20809  obsipid  20974  smadiadetlem2  21858  smadiadet  21864  ordtt1  22575  xmet0  23540  nmsq  24403  tcphcphlem3  24442  tcphcph  24446  grpoidinvlem1  28911  grpodivid  28949  nvmid  29066  ipidsq  29117  5oalem1  30061  3oalem2  30070  unopf1o  30323  unopnorm  30324  hmopre  30330  ballotlemfc0  32504  ballotlemfcc  32505  gcdabsorb  33761  cgr3rflx  34401  endofsegid  34432  tailini  34610  nnssi2  34689  nndivlub  34692  brin2  36577  opoccl  37250  opococ  37251  opexmid  37263  opnoncon  37264  cmtidN  37313  ltrniotaidvalN  38639  pell14qrexpclnn0  40725  rmxdbl  40799  rmydbl  40800  rhmsubclem3  45704  rhmsubcALTVlem3  45722