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  7215  cfcof  10187  axcclem  10370  enqeq  10848  leltletr  11228  ltleletr  11230  ixxssixx  13303  prodmolem2  15891  prodmo  15892  zprod  15893  muldvds1  16240  dvds2add  16250  dvds2sub  16251  dvdstr  16254  initoeu2lem2  17973  pospropd  18282  mndissubm  18766  csrgbinom  20204  smadiadetglem2  22647  ismbf3d  25631  mbfi1flimlem  25699  colinearalg  28993  frusgrnn0  29655  2wlkond  30020  2pthond  30025  2pthon3v  30026  umgr2adedgwlkonALT  30030  vdgn1frgrv2  30381  frgr2wwlkeqm  30416  bnj967  35103  bnj1110  35140  fineqvinfep  35285  subgrwlk  35330  cgr3permute3  36245  cgr3com  36251  brofs2  36275  bj-idreseq  37492  areacirclem4  38046  paddasslem14  40293  lhpexle1  40468  cdlemk19w  41432  ismrc  43147  iocinico  43658  gneispb  44576  fourierdlem113  46665  sigaras  47301  sigarms  47302  plusmod5ne  47811  gpgusgralem  48544  lincresunit3lem3  48962  lincresunit3  48969