Theorem 3simpb 1165

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 23	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ 𝜒))
2	1	3adant2 1147	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3adantl2  1184  3adantr2  1187  fpropnf1  7255  cfcof  10246  axcclem  10429  enqeq  10907  leltletr  11289  ltleletr  11291  ixxssixx  13374  prodmolem2  15977  prodmo  15978  zprod  15979  muldvds1  16326  dvds2add  16336  dvds2sub  16337  dvdstr  16340  initoeu2lem2  18060  pospropd  18369  mndissubm  18853  csrgbinom  20302  smadiadetglem2  22786  ismbf3d  25770  mbfi1flimlem  25838  colinearalg  29165  frusgrnn0  29826  2wlkond  30191  2pthond  30196  2pthon3v  30197  umgr2adedgwlkonALT  30201  vdgn1frgrv2  30552  frgr2wwlkeqm  30587  bnj967  35245  bnj1110  35282  fineqvinfep  35428  subgrwlk  35490  cgr3permute3  36405  cgr3com  36411  brofs2  36435  bj-idreseq  37661  areacirclem4  38217  paddasslem14  40464  lhpexle1  40639  cdlemk19w  41603  ismrc  43289  iocinico  43796  gneispb  44714  fourierdlem113  46792  sigaras  47428  sigarms  47429  plusmod5ne  47944  gpgusgralem  48677  lincresunit3lem3  49106  lincresunit3  49113