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  7208  cfcof  10187  axcclem  10370  enqeq  10847  leltletr  11225  ltleletr  11227  ixxssixx  13280  prodmolem2  15860  prodmo  15861  zprod  15862  muldvds1  16209  dvds2add  16219  dvds2sub  16220  dvdstr  16223  initoeu2lem2  17940  pospropd  18249  mndissubm  18699  csrgbinom  20135  smadiadetglem2  22575  ismbf3d  25571  mbfi1flimlem  25639  colinearalg  28873  frusgrnn0  29535  2wlkond  29900  2pthond  29905  2pthon3v  29906  umgr2adedgwlkonALT  29910  vdgn1frgrv2  30258  frgr2wwlkeqm  30293  bnj967  34914  bnj1110  34951  subgrwlk  35107  cgr3permute3  36023  cgr3com  36029  brofs2  36053  bj-idreseq  37138  areacirclem4  37693  paddasslem14  39815  lhpexle1  39990  cdlemk19w  40954  ismrc  42677  iocinico  43188  gneispb  44107  fourierdlem113  46204  sigaras  46840  sigarms  46841  plusmod5ne  47333  gpgusgralem  48044  lincresunit3lem3  48463  lincresunit3  48470