Theorem 3simpb 1161

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3adantl2  1180  3adantr2  1183  fpropnf1  7245  cfcof  10224  axcclem  10407  enqeq  10885  leltletr  11267  ltleletr  11269  ixxssixx  13356  prodmolem2  15955  prodmo  15956  zprod  15957  muldvds1  16304  dvds2add  16314  dvds2sub  16315  dvdstr  16318  initoeu2lem2  18038  pospropd  18347  mndissubm  18831  csrgbinom  20268  smadiadetglem2  22719  ismbf3d  25703  mbfi1flimlem  25771  colinearalg  29067  frusgrnn0  29728  2wlkond  30093  2pthond  30098  2pthon3v  30099  umgr2adedgwlkonALT  30103  vdgn1frgrv2  30454  frgr2wwlkeqm  30489  bnj967  35200  bnj1110  35237  fineqvinfep  35381  subgrwlk  35442  cgr3permute3  36357  cgr3com  36363  brofs2  36387  bj-idreseq  37614  areacirclem4  38170  paddasslem14  40417  lhpexle1  40592  cdlemk19w  41556  ismrc  43242  iocinico  43749  gneispb  44667  fourierdlem113  46753  sigaras  47389  sigarms  47390  plusmod5ne  47905  gpgusgralem  48638  lincresunit3lem3  49056  lincresunit3  49063