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  1167  3adantr2  1170  fpropnf1  7269  cfcof  10296  axcclem  10479  enqeq  10956  leltletr  11334  ltleletr  11336  ixxssixx  13383  prodmolem2  15954  prodmo  15955  zprod  15956  muldvds1  16301  dvds2add  16310  dvds2sub  16311  dvdstr  16314  initoeu2lem2  18032  pospropd  18342  mndissubm  18790  csrgbinom  20198  smadiadetglem2  22627  ismbf3d  25626  mbfi1flimlem  25694  colinearalg  28856  frusgrnn0  29518  2wlkond  29886  2pthond  29891  2pthon3v  29892  umgr2adedgwlkonALT  29896  vdgn1frgrv2  30244  frgr2wwlkeqm  30279  bnj967  34934  bnj1110  34971  subgrwlk  35112  cgr3permute3  36023  cgr3com  36029  brofs2  36053  bj-idreseq  37138  areacirclem4  37693  paddasslem14  39810  lhpexle1  39985  cdlemk19w  40949  ismrc  42690  iocinico  43202  gneispb  44121  fourierdlem113  46206  sigaras  46842  sigarms  46843  plusmod5ne  47320  gpgusgralem  47984  lincresunit3lem3  48364  lincresunit3  48371