Theorem 3simpb 1057

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3simpb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Proof of Theorem 3simpb

Step	Hyp	Ref	Expression
1		3ancomb 1045	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
2		3simpa 1056	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝜑 ∧ 𝜒))
3	1, 2	sylbi 207	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  3adant2  1078  3adantl2  1216  3adantr2  1219  fpropnf1  6479  cfcof  9041  axcclem  9224  enqeq  9701  ltleletr  10075  ixxssixx  12128  prodmolem2  14585  prodmo  14586  zprod  14587  muldvds1  14925  dvds2add  14934  dvds2sub  14935  dvdstr  14937  initoeu2lem2  16581  pospropd  17050  csrgbinom  18462  smadiadetglem2  20392  ismbf3d  23322  mbfi1flimlem  23390  colinearalg  25685  frusgrnn0  26331  wlkwwlkinj  26645  2wlkond  26696  2pthond  26701  2pthon3v  26702  umgr2adedgwlkonALT  26706  usgr2wspthons3  26719  vdgn1frgrv2  27018  extwwlkfab  27072  bnj967  30715  bnj1110  30750  cgr3permute3  31788  cgr3com  31794  brofs2  31818  areacirclem4  33121  paddasslem14  34585  lhpexle1  34760  cdlemk19w  35726  ismrc  36730  iocinico  37264  gneispb  37897  fourierdlem113  39730  sigaras  40335  sigarms  40336  leltletr  40593  lincresunit3lem3  41525  lincresunit3  41532