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

Theorem 3simpc 1080
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
3simpc ((𝜑𝜓𝜒) → (𝜓𝜒))

Proof of Theorem 3simpc
StepHypRef Expression
1 3anrot 1060 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
2 3simpa 1078 . 2 ((𝜓𝜒𝜑) → (𝜓𝜒))
31, 2sylbi 207 1 ((𝜑𝜓𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  simp3  1083  3adant1  1099  3adantl1  1237  3adantr1  1240  pr1eqbg  4421  fpropnf1  6564  find  7133  tz7.49c  7586  eqsup  8403  fimin2g  8444  mulcanenq  9820  elnpi  9848  divcan2  10731  diveq0  10733  divrec  10739  divcan3  10749  eliooord  12271  fzrev3  12444  modaddabs  12748  modaddmod  12749  muladdmodid  12750  modmulmod  12775  sqdiv  12968  swrdlend  13477  swrdnd  13478  ccats1swrdeqbi  13544  sqrmo  14036  muldvds2  15054  dvdscmul  15055  dvdsmulc  15056  dvdstr  15065  funcestrcsetclem9  16835  funcsetcestrclem9  16850  domneq0  19345  aspid  19378  znleval2  19952  redvr  20011  scmatscmiddistr  20362  1marepvmarrepid  20429  mat2pmatghm  20583  pmatcollpw1lem1  20627  monmatcollpw  20632  pmatcollpwscmatlem2  20643  conncompss  21284  islly2  21335  elmptrab2  21679  tngngp3  22507  lmmcvg  23105  ivthicc  23273  aaliou3lem7  24149  logimcl  24361  qrngdiv  25358  ax5seg  25863  uhgr2edg  26145  umgr2edgneu  26151  uspgr1ewop  26185  iswlkg  26565  wlkonprop  26610  wlkonwlk  26614  trlsonprop  26660  trlontrl  26663  upgrwlkdvspth  26691  pthsonprop  26696  spthonprop  26697  pthonpth  26700  spthonpthon  26703  uhgrwkspth  26707  usgr2wlkspthlem1  26709  usgr2wlkspthlem2  26710  usgr2wlkspth  26711  wwlknbp2OLD  26794  2pthon3v  26908  umgr2wlk  26914  rusgrnumwwlkg  26943  clwwisshclwws  26972  clwwlknp  26999  clwwlkfo  27013  clwwlknwwlkncl  27016  clwwlknwwlknclOLD  27017  clwlksfclwwlk  27049  clwlksf1clwwlklem  27055  1pthond  27122  uhgr3cyclex  27160  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  numclwwlk3  27372  ajfuni  27843  funadj  28873  fovcld  29568  trleile  29794  isinftm  29863  bnj1098  30980  bnj546  31092  bnj998  31152  bnj1006  31155  bnj1173  31196  bnj1189  31203  cgr3permute1  32280  cgr3com  32285  brifs2  32310  idinside  32316  btwnconn1  32333  lineunray  32379  wl-nfeqfb  33453  riotasv2s  34562  lsatlspsn2  34597  3dim2  35072  paddasslem14  35437  4atexlemex6  35678  cdlemg10bALTN  36241  cdlemg44  36338  tendoplcl  36386  hdmap14lem14  37490  pm13.194  38930  fmulcl  40131  fmuldfeqlem1  40132  stoweidlem17  40552  stoweidlem31  40566  dfsalgen2  40877  sigaraf  41363  sigarmf  41364  elfzelfzlble  41656  ccats1pfxeqbi  41756  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  zlmodzxzscm  42460  divsub1dir  42632  elbigoimp  42675  digexp  42726
  Copyright terms: Public domain W3C validator