Theorem 3simpb 1147

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3adantl2  1165  3adantr2  1168  fpropnf1  7134  cfcof  10014  axcclem  10197  enqeq  10674  ltleletr  11051  ixxssixx  13075  prodmolem2  15626  prodmo  15627  zprod  15628  muldvds1  15971  dvds2add  15980  dvds2sub  15981  dvdstr  15984  initoeu2lem2  17711  pospropd  18026  mndissubm  18427  csrgbinom  19763  smadiadetglem2  21802  ismbf3d  24799  mbfi1flimlem  24868  colinearalg  27259  frusgrnn0  27919  2wlkond  28281  2pthond  28286  2pthon3v  28287  umgr2adedgwlkonALT  28291  vdgn1frgrv2  28639  frgr2wwlkeqm  28674  bnj967  32904  bnj1110  32941  subgrwlk  33073  cgr3permute3  34328  cgr3com  34334  brofs2  34358  bj-idreseq  35312  areacirclem4  35847  paddasslem14  37826  lhpexle1  38001  cdlemk19w  38965  ismrc  40503  iocinico  41023  gneispb  41694  fourierdlem113  43714  sigaras  44322  sigarms  44323  leltletr  44737  lincresunit3lem3  45767  lincresunit3  45774