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 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  3adantl2  1167  3adantr2  1170  fpropnf1  7172  cfcof  10076  axcclem  10259  enqeq  10736  leltletr  11112  ltleletr  11114  ixxssixx  13139  prodmolem2  15690  prodmo  15691  zprod  15692  muldvds1  16035  dvds2add  16044  dvds2sub  16045  dvdstr  16048  initoeu2lem2  17775  pospropd  18090  mndissubm  18491  csrgbinom  19827  smadiadetglem2  21866  ismbf3d  24863  mbfi1flimlem  24932  colinearalg  27323  frusgrnn0  27983  2wlkond  28347  2pthond  28352  2pthon3v  28353  umgr2adedgwlkonALT  28357  vdgn1frgrv2  28705  frgr2wwlkeqm  28740  bnj967  32970  bnj1110  33007  subgrwlk  33139  cgr3permute3  34394  cgr3com  34400  brofs2  34424  bj-idreseq  35377  areacirclem4  35912  paddasslem14  37889  lhpexle1  38064  cdlemk19w  39028  ismrc  40560  iocinico  41081  gneispb  41779  fourierdlem113  43809  sigaras  44429  sigarms  44430  lincresunit3lem3  45873  lincresunit3  45880