MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3simpb Structured version   Visualization version   GIF version

Theorem 3simpb 1057
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3simpb ((𝜑𝜓𝜒) → (𝜑𝜒))

Proof of Theorem 3simpb
StepHypRef Expression
1 3ancomb 1045 . 2 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
2 3simpa 1056 . 2 ((𝜑𝜒𝜓) → (𝜑𝜒))
31, 2sylbi 207 1 ((𝜑𝜓𝜒) → (𝜑𝜒))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator