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 395   ∧ w3a 1086

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

This theorem is referenced by:  3adantl2  1168  3adantr2  1171  fpropnf1  7242  cfcof  10227  axcclem  10410  enqeq  10887  leltletr  11265  ltleletr  11267  ixxssixx  13320  prodmolem2  15901  prodmo  15902  zprod  15903  muldvds1  16250  dvds2add  16260  dvds2sub  16261  dvdstr  16264  initoeu2lem2  17977  pospropd  18286  mndissubm  18734  csrgbinom  20141  smadiadetglem2  22559  ismbf3d  25555  mbfi1flimlem  25623  colinearalg  28837  frusgrnn0  29499  2wlkond  29867  2pthond  29872  2pthon3v  29873  umgr2adedgwlkonALT  29877  vdgn1frgrv2  30225  frgr2wwlkeqm  30260  bnj967  34935  bnj1110  34972  subgrwlk  35119  cgr3permute3  36035  cgr3com  36041  brofs2  36065  bj-idreseq  37150  areacirclem4  37705  paddasslem14  39827  lhpexle1  40002  cdlemk19w  40966  ismrc  42689  iocinico  43201  gneispb  44120  fourierdlem113  46217  sigaras  46853  sigarms  46854  plusmod5ne  47346  gpgusgralem  48047  lincresunit3lem3  48463  lincresunit3  48470