Theorem 3simpb 1150

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 1090

This theorem is referenced by:  3adantl2  1168  3adantr2  1171  fpropnf1  7266  cfcof  10269  axcclem  10452  enqeq  10929  leltletr  11305  ltleletr  11307  ixxssixx  13338  prodmolem2  15879  prodmo  15880  zprod  15881  muldvds1  16224  dvds2add  16233  dvds2sub  16234  dvdstr  16237  initoeu2lem2  17965  pospropd  18280  mndissubm  18688  csrgbinom  20055  smadiadetglem2  22174  ismbf3d  25171  mbfi1flimlem  25240  colinearalg  28199  frusgrnn0  28859  2wlkond  29222  2pthond  29227  2pthon3v  29228  umgr2adedgwlkonALT  29232  vdgn1frgrv2  29580  frgr2wwlkeqm  29615  bnj967  33987  bnj1110  34024  subgrwlk  34154  cgr3permute3  35050  cgr3com  35056  brofs2  35080  gg-cncrng  35231  bj-idreseq  36091  areacirclem4  36627  paddasslem14  38752  lhpexle1  38927  cdlemk19w  39891  ismrc  41487  iocinico  42009  gneispb  42930  fourierdlem113  44983  sigaras  45619  sigarms  45620  lincresunit3lem3  47203  lincresunit3  47210