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

This theorem is referenced by:  3adantl2  1167  3adantr2  1170  fpropnf1  7304  cfcof  10343  axcclem  10526  enqeq  11003  leltletr  11381  ltleletr  11383  ixxssixx  13421  prodmolem2  15983  prodmo  15984  zprod  15985  muldvds1  16329  dvds2add  16338  dvds2sub  16339  dvdstr  16342  initoeu2lem2  18082  pospropd  18397  mndissubm  18842  csrgbinom  20259  smadiadetglem2  22699  ismbf3d  25708  mbfi1flimlem  25777  colinearalg  28943  frusgrnn0  29607  2wlkond  29970  2pthond  29975  2pthon3v  29976  umgr2adedgwlkonALT  29980  vdgn1frgrv2  30328  frgr2wwlkeqm  30363  bnj967  34921  bnj1110  34958  subgrwlk  35100  cgr3permute3  36011  cgr3com  36017  brofs2  36041  bj-idreseq  37128  areacirclem4  37671  paddasslem14  39790  lhpexle1  39965  cdlemk19w  40929  ismrc  42657  iocinico  43173  gneispb  44093  fourierdlem113  46140  sigaras  46776  sigarms  46777  lincresunit3lem3  48203  lincresunit3  48210