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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3adantl2  1186  3adantr2  1189  fpropnf1  7267  cfcof  10259  axcclem  10442  enqeq  10920  leltletr  11302  ltleletr  11304  ixxssixx  13387  prodmolem2  15991  prodmo  15992  zprod  15993  muldvds1  16339  dvds2add  16349  dvds2sub  16350  dvdstr  16353  initoeu2lem2  18073  pospropd  18382  mndissubm  18866  csrgbinom  20315  smadiadetglem2  22810  ismbf3d  25794  mbfi1flimlem  25862  colinearalg  29241  frusgrnn0  29902  2wlkond  30267  2pthond  30272  2pthon3v  30273  umgr2adedgwlkonALT  30277  vdgn1frgrv2  30628  frgr2wwlkeqm  30663  bnj967  35314  bnj1110  35351  fineqvinfep  35519  subgrwlk  35605  cgr3permute3  36520  cgr3com  36526  brofs2  36550  bj-idreseq  37787  areacirclem4  38343  paddasslem14  40588  lhpexle1  40763  cdlemk19w  41727  ismrc  43415  iocinico  43922  gneispb  44840  fourierdlem113  46916  sigaras  47552  sigarms  47553  plusmod5ne  48071  gpgusgralem  48804  lincresunit3lem3  49237  lincresunit3  49244