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  1168  3adantr2  1171  fpropnf1  7285  cfcof  10310  axcclem  10493  enqeq  10970  leltletr  11348  ltleletr  11350  ixxssixx  13397  prodmolem2  15967  prodmo  15968  zprod  15969  muldvds1  16314  dvds2add  16323  dvds2sub  16324  dvdstr  16327  initoeu2lem2  18056  pospropd  18368  mndissubm  18816  csrgbinom  20225  smadiadetglem2  22668  ismbf3d  25679  mbfi1flimlem  25747  colinearalg  28915  frusgrnn0  29579  2wlkond  29947  2pthond  29952  2pthon3v  29953  umgr2adedgwlkonALT  29957  vdgn1frgrv2  30305  frgr2wwlkeqm  30340  bnj967  34937  bnj1110  34974  subgrwlk  35115  cgr3permute3  36026  cgr3com  36032  brofs2  36056  bj-idreseq  37141  areacirclem4  37696  paddasslem14  39813  lhpexle1  39988  cdlemk19w  40952  ismrc  42690  iocinico  43202  gneispb  44122  fourierdlem113  46207  sigaras  46843  sigarms  46844  plusmod5ne  47320  gpgusgralem  47984  lincresunit3lem3  48364  lincresunit3  48371