Theorem 3simpb 1167

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 23	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ 𝜒))
2	1	3adant2 1149	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adantl2  1186  3adantr2  1189  fpropnf1  7264  cfcof  10276  axcclem  10459  enqeq  10943  leltletr  11325  ltleletr  11327  ixxssixx  13412  prodmolem2  16022  prodmo  16023  zprod  16024  muldvds1  16370  dvds2add  16380  dvds2sub  16381  dvdstr  16384  initoeu2lem2  18104  pospropd  18413  mndissubm  18915  csrgbinom  20371  smadiadetglem2  22894  ismbf3d  25882  mbfi1flimlem  25950  colinearalg  29367  frusgrnn0  30031  subgrwlk  30148  2wlkond  30405  2pthond  30410  2pthon3v  30411  umgr2adedgwlkonALT  30415  vdgn1frgrv2  30776  frgr2wwlkeqm  30811  bnj967  35454  bnj1110  35491  fineqvinfep  35651  cgr3permute3  36627  cgr3com  36633  brofs2  36657  bj-idreseq  37914  areacirclem4  38460  paddasslem14  40706  lhpexle1  40881  cdlemk19w  41845  ismrc  43546  iocinico  44053  gneispb  44971  fourierdlem113  47047  sigaras  47683  sigarms  47684  plusmod5ne  48239  gpgusgralem  48972  lincresunit3lem3  49404  lincresunit3  49411