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  7272  cfcof  10356  axcclem  10539  enqeq  11023  leltletr  11405  ltleletr  11407  ixxssixx  13494  prodmolem2  16108  prodmo  16109  zprod  16110  muldvds1  16456  dvds2add  16466  dvds2sub  16467  dvdstr  16470  initoeu2lem2  18196  pospropd  18505  mndissubm  19008  csrgbinom  20464  smadiadetglem2  22993  ismbf3d  25981  mbfi1flimlem  26049  colinearalg  29494  frusgrnn0  30158  subgrwlk  30275  2wlkond  30532  2pthond  30537  2pthon3v  30538  umgr2adedgwlkonALT  30542  vdgn1frgrv2  30903  frgr2wwlkeqm  30938  bnj967  35622  bnj1110  35659  fineqvinfep  35850  cgr3permute3  36905  cgr3com  36911  brofs2  36935  bj-idreseq  38177  areacirclem4  38723  paddasslem14  40984  lhpexle1  41159  cdlemk19w  42123  ismrc  43806  iocinico  44308  gneispb  45225  fourierdlem113  47323  sigaras  47959  sigarms  47960  plusmod5ne  48515  gpgusgralem  49248  lincresunit3lem3  49680  lincresunit3  49687