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  7201  cfcof  10165  axcclem  10348  enqeq  10825  leltletr  11204  ltleletr  11206  ixxssixx  13259  prodmolem2  15842  prodmo  15843  zprod  15844  muldvds1  16191  dvds2add  16201  dvds2sub  16202  dvdstr  16205  initoeu2lem2  17922  pospropd  18231  mndissubm  18715  csrgbinom  20150  smadiadetglem2  22587  ismbf3d  25582  mbfi1flimlem  25650  colinearalg  28888  frusgrnn0  29550  2wlkond  29915  2pthond  29920  2pthon3v  29921  umgr2adedgwlkonALT  29925  vdgn1frgrv2  30276  frgr2wwlkeqm  30311  bnj967  34957  bnj1110  34994  subgrwlk  35176  cgr3permute3  36091  cgr3com  36097  brofs2  36121  bj-idreseq  37206  areacirclem4  37761  paddasslem14  39942  lhpexle1  40117  cdlemk19w  41081  ismrc  42804  iocinico  43315  gneispb  44234  fourierdlem113  46327  sigaras  46963  sigarms  46964  plusmod5ne  47455  gpgusgralem  48166  lincresunit3lem3  48585  lincresunit3  48592