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 400   ∧ 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 401  df-3an 1105

This theorem is used by:  3adantl2  1186  3adantr2  1189  fpropnf1  7265  cfcof  10262  axcclem  10445  enqeq  10923  leltletr  11305  ltleletr  11307  ixxssixx  13390  prodmolem2  15994  prodmo  15995  zprod  15996  muldvds1  16342  dvds2add  16352  dvds2sub  16353  dvdstr  16356  initoeu2lem2  18076  pospropd  18385  mndissubm  18869  csrgbinom  20318  smadiadetglem2  22838  ismbf3d  25822  mbfi1flimlem  25890  colinearalg  29269  frusgrnn0  29930  2wlkond  30295  2pthond  30300  2pthon3v  30301  umgr2adedgwlkonALT  30305  vdgn1frgrv2  30656  frgr2wwlkeqm  30691  bnj967  35342  bnj1110  35379  fineqvinfep  35546  subgrwlk  35632  cgr3permute3  36547  cgr3com  36553  brofs2  36577  bj-idreseq  37834  areacirclem4  38390  paddasslem14  40635  lhpexle1  40810  cdlemk19w  41774  ismrc  43460  iocinico  43967  gneispb  44885  fourierdlem113  46961  sigaras  47597  sigarms  47598  plusmod5ne  48116  gpgusgralem  48849  lincresunit3lem3  49282  lincresunit3  49289