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  7222  cfcof  10196  axcclem  10379  enqeq  10857  leltletr  11237  ltleletr  11239  ixxssixx  13312  prodmolem2  15900  prodmo  15901  zprod  15902  muldvds1  16249  dvds2add  16259  dvds2sub  16260  dvdstr  16263  initoeu2lem2  17982  pospropd  18291  mndissubm  18775  csrgbinom  20213  smadiadetglem2  22637  ismbf3d  25621  mbfi1flimlem  25689  colinearalg  28979  frusgrnn0  29640  2wlkond  30005  2pthond  30010  2pthon3v  30011  umgr2adedgwlkonALT  30015  vdgn1frgrv2  30366  frgr2wwlkeqm  30401  bnj967  35087  bnj1110  35124  fineqvinfep  35269  subgrwlk  35314  cgr3permute3  36229  cgr3com  36235  brofs2  36259  bj-idreseq  37476  areacirclem4  38032  paddasslem14  40279  lhpexle1  40454  cdlemk19w  41418  ismrc  43133  iocinico  43640  gneispb  44558  fourierdlem113  46647  sigaras  47283  sigarms  47284  plusmod5ne  47799  gpgusgralem  48532  lincresunit3lem3  48950  lincresunit3  48957