Theorem 3simpb 1149

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  3adantl2  1167  3adantr2  1170  fpropnf1  7210  cfcof  10168  axcclem  10351  enqeq  10828  leltletr  11204  ltleletr  11206  ixxssixx  13232  prodmolem2  15778  prodmo  15779  zprod  15780  muldvds1  16123  dvds2add  16132  dvds2sub  16133  dvdstr  16136  initoeu2lem2  17861  pospropd  18176  mndissubm  18578  csrgbinom  19917  smadiadetglem2  21973  ismbf3d  24970  mbfi1flimlem  25039  colinearalg  27688  frusgrnn0  28348  2wlkond  28711  2pthond  28716  2pthon3v  28717  umgr2adedgwlkonALT  28721  vdgn1frgrv2  29069  frgr2wwlkeqm  29104  bnj967  33369  bnj1110  33406  subgrwlk  33538  cgr3permute3  34570  cgr3com  34576  brofs2  34600  bj-idreseq  35571  areacirclem4  36107  paddasslem14  38234  lhpexle1  38409  cdlemk19w  39373  ismrc  40933  iocinico  41455  gneispb  42314  fourierdlem113  44361  sigaras  44997  sigarms  44998  lincresunit3lem3  46456  lincresunit3  46463