Theorem 3simpb 1150

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adantl2  1169  3adantr2  1172  fpropnf1  7223  cfcof  10196  axcclem  10379  enqeq  10857  leltletr  11236  ltleletr  11238  ixxssixx  13287  prodmolem2  15870  prodmo  15871  zprod  15872  muldvds1  16219  dvds2add  16229  dvds2sub  16230  dvdstr  16233  initoeu2lem2  17951  pospropd  18260  mndissubm  18744  csrgbinom  20179  smadiadetglem2  22628  ismbf3d  25623  mbfi1flimlem  25691  colinearalg  28995  frusgrnn0  29657  2wlkond  30022  2pthond  30027  2pthon3v  30028  umgr2adedgwlkonALT  30032  vdgn1frgrv2  30383  frgr2wwlkeqm  30418  bnj967  35120  bnj1110  35157  fineqvinfep  35300  subgrwlk  35345  cgr3permute3  36260  cgr3com  36266  brofs2  36290  bj-idreseq  37414  areacirclem4  37959  paddasslem14  40206  lhpexle1  40381  cdlemk19w  41345  ismrc  43055  iocinico  43566  gneispb  44484  fourierdlem113  46574  sigaras  47210  sigarms  47211  plusmod5ne  47702  gpgusgralem  48413  lincresunit3lem3  48831  lincresunit3  48838