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  7244  cfcof  10233  axcclem  10416  enqeq  10893  leltletr  11271  ltleletr  11273  ixxssixx  13326  prodmolem2  15907  prodmo  15908  zprod  15909  muldvds1  16256  dvds2add  16266  dvds2sub  16267  dvdstr  16270  initoeu2lem2  17983  pospropd  18292  mndissubm  18740  csrgbinom  20147  smadiadetglem2  22565  ismbf3d  25561  mbfi1flimlem  25629  colinearalg  28843  frusgrnn0  29505  2wlkond  29873  2pthond  29878  2pthon3v  29879  umgr2adedgwlkonALT  29883  vdgn1frgrv2  30231  frgr2wwlkeqm  30266  bnj967  34941  bnj1110  34978  subgrwlk  35119  cgr3permute3  36030  cgr3com  36036  brofs2  36060  bj-idreseq  37145  areacirclem4  37700  paddasslem14  39822  lhpexle1  39997  cdlemk19w  40961  ismrc  42682  iocinico  43194  gneispb  44113  fourierdlem113  46210  sigaras  46846  sigarms  46847  plusmod5ne  47336  gpgusgralem  48037  lincresunit3lem3  48453  lincresunit3  48460