Theorem 3simpb 1149

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Assertion

Ref	Expression
3simpb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Proof of Theorem 3simpb

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ 𝜒))
2	1	3adant2 1131	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:  3adantl2  1168  3adantr2  1171  fpropnf1  7201  cfcof  10165  axcclem  10348  enqeq  10825  leltletr  11204  ltleletr  11206  ixxssixx  13259  prodmolem2  15842  prodmo  15843  zprod  15844  muldvds1  16191  dvds2add  16201  dvds2sub  16202  dvdstr  16205  initoeu2lem2  17922  pospropd  18231  mndissubm  18715  csrgbinom  20151  smadiadetglem2  22588  ismbf3d  25583  mbfi1flimlem  25651  colinearalg  28889  frusgrnn0  29551  2wlkond  29916  2pthond  29921  2pthon3v  29922  umgr2adedgwlkonALT  29926  vdgn1frgrv2  30274  frgr2wwlkeqm  30309  bnj967  34955  bnj1110  34992  subgrwlk  35174  cgr3permute3  36087  cgr3com  36093  brofs2  36117  bj-idreseq  37202  areacirclem4  37757  paddasslem14  39878  lhpexle1  40053  cdlemk19w  41017  ismrc  42740  iocinico  43251  gneispb  44170  fourierdlem113  46263  sigaras  46899  sigarms  46900  plusmod5ne  47382  gpgusgralem  48093  lincresunit3lem3  48512  lincresunit3  48519