Theorem 3simpb 1145

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3adantl2  1163  3adantr2  1166  fpropnf1  7027  cfcof  9698  axcclem  9881  enqeq  10358  ltleletr  10735  ixxssixx  12755  prodmolem2  15291  prodmo  15292  zprod  15293  muldvds1  15636  dvds2add  15645  dvds2sub  15646  dvdstr  15648  initoeu2lem2  17277  pospropd  17746  mndissubm  17974  csrgbinom  19298  smadiadetglem2  21283  ismbf3d  24257  mbfi1flimlem  24325  colinearalg  26698  frusgrnn0  27355  2wlkond  27718  2pthond  27723  2pthon3v  27724  umgr2adedgwlkonALT  27728  vdgn1frgrv2  28077  frgr2wwlkeqm  28112  bnj967  32219  bnj1110  32256  subgrwlk  32381  cgr3permute3  33510  cgr3com  33516  brofs2  33540  bj-idreseq  34456  areacirclem4  34987  paddasslem14  36971  lhpexle1  37146  cdlemk19w  38110  ismrc  39305  iocinico  39825  gneispb  40488  fourierdlem113  42511  sigaras  43119  sigarms  43120  leltletr  43500  lincresunit3lem3  44536  lincresunit3  44543