Theorem 3simpb 1146

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3adantl2  1164  3adantr2  1167  fpropnf1  7017  cfcof  9734  axcclem  9917  enqeq  10394  ltleletr  10771  ixxssixx  12793  prodmolem2  15337  prodmo  15338  zprod  15339  muldvds1  15682  dvds2add  15691  dvds2sub  15692  dvdstr  15695  initoeu2lem2  17341  pospropd  17810  mndissubm  18038  csrgbinom  19364  smadiadetglem2  21372  ismbf3d  24354  mbfi1flimlem  24422  colinearalg  26803  frusgrnn0  27460  2wlkond  27822  2pthond  27827  2pthon3v  27828  umgr2adedgwlkonALT  27832  vdgn1frgrv2  28180  frgr2wwlkeqm  28215  bnj967  32445  bnj1110  32482  subgrwlk  32610  cgr3permute3  33898  cgr3com  33904  brofs2  33928  bj-idreseq  34857  areacirclem4  35428  paddasslem14  37409  lhpexle1  37584  cdlemk19w  38548  ismrc  40015  iocinico  40535  gneispb  41207  fourierdlem113  43227  sigaras  43835  sigarms  43836  leltletr  44218  lincresunit3lem3  45248  lincresunit3  45255