Theorem 3simpb 1145

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3adant2OLD  1153  3adantl2  1173  3adantr2  1176  fpropnf1  6687  cfcof  9288  axcclem  9471  enqeq  9948  ltleletr  10322  ixxssixx  12382  prodmolem2  14864  prodmo  14865  zprod  14866  muldvds1  15208  dvds2add  15217  dvds2sub  15218  dvdstr  15220  initoeu2lem2  16866  pospropd  17335  csrgbinom  18746  smadiadetglem2  20680  ismbf3d  23620  mbfi1flimlem  23688  colinearalg  25989  frusgrnn0  26677  wlkwwlkinj  27005  2wlkond  27057  2pthond  27062  2pthon3v  27063  umgr2adedgwlkonALT  27067  vdgn1frgrv2  27450  frgr2wwlkeqm  27485  bnj967  31322  bnj1110  31357  cgr3permute3  32460  cgr3com  32466  brofs2  32490  areacirclem4  33816  paddasslem14  35622  lhpexle1  35797  cdlemk19w  36762  ismrc  37766  iocinico  38299  gneispb  38931  fourierdlem113  40939  sigaras  41550  sigarms  41551  leltletr  41818  lincresunit3lem3  42773  lincresunit3  42780