Theorem 3simpb 1167

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adantl2  1186  3adantr2  1189  fpropnf1  7300  cfcof  10389  axcclem  10572  enqeq  11056  leltletr  11438  ltleletr  11440  ixxssixx  13528  prodmolem2  16143  prodmo  16144  zprod  16145  muldvds1  16491  dvds2add  16501  dvds2sub  16502  dvdstr  16505  initoeu2lem2  18231  pospropd  18540  mndissubm  19043  csrgbinom  20500  smadiadetglem2  23031  ismbf3d  26019  mbfi1flimlem  26087  colinearalg  29534  frusgrnn0  30198  subgrwlk  30315  2wlkond  30572  2pthond  30577  2pthon3v  30578  umgr2adedgwlkonALT  30582  vdgn1frgrv2  30943  frgr2wwlkeqm  30978  bnj967  35679  bnj1110  35716  fineqvinfep  35927  cgr3permute3  37020  cgr3com  37026  brofs2  37050  bj-idreseq  38344  areacirclem4  38890  paddasslem14  41149  lhpexle1  41324  cdlemk19w  42288  ismrc  43972  iocinico  44469  gneispb  45386  fourierdlem113  47496  sigaras  48132  sigarms  48133  plusmod5ne  48688  gpgusgralem  49421  lincresunit3lem3  49911  lincresunit3  49918