Theorem 3simpb 1142

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 1123	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  1150  3adantl2  1153  3adantr2  1156  3imp3i2an  1401  fpropnf1  6639  cfcof  9209  axcclem  9392  enqeq  9869  ltleletr  10243  ixxssixx  12303  prodmolem2  14785  prodmo  14786  zprod  14787  muldvds1  15129  dvds2add  15138  dvds2sub  15139  dvdstr  15141  initoeu2lem2  16787  pospropd  17256  csrgbinom  18667  smadiadetglem2  20601  ismbf3d  23541  mbfi1flimlem  23609  colinearalg  25910  frusgrnn0  26598  wlkwwlkinj  26926  2wlkond  26978  2pthond  26983  2pthon3v  26984  umgr2adedgwlkonALT  26988  vdgn1frgrv2  27371  frgr2wwlkeqm  27406  bnj967  31243  bnj1110  31278  cgr3permute3  32381  cgr3com  32387  brofs2  32411  areacirclem4  33735  paddasslem14  35539  lhpexle1  35714  cdlemk19w  36679  ismrc  37683  iocinico  38216  gneispb  38848  fourierdlem113  40856  sigaras  41467  sigarms  41468  leltletr  41735  lincresunit3lem3  42690  lincresunit3  42697