MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com13 Unicode version

Theorem com13 76
Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
com13  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3r 75 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com23 74 1  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com24  83  an13s  779  an31s  782  meredith  1410  peano5  4827  funopg  5444  eldmrexrnb  5836  f1o2ndf1  6413  abianfp  6675  omordi  6768  omeulem1  6784  brecop  6956  isinf  7281  fiint  7342  carduni  7824  dfac5  7965  dfac2  7967  cofsmo  8105  cfcoflem  8108  domtriomlem  8278  axdc3lem2  8287  nqereu  8762  squeeze0  9869  zmax  10527  xrsupsslem  10841  xrinfmsslem  10842  supxrunb1  10854  supxrunb2  10855  difreicc  10984  elfznelfzo  11147  injresinjlem  11154  injresinj  11155  uzindi  11275  facwordi  11535  hasheqf1oi  11590  hashf1rn  11591  hash2prde  11643  sqr2irr  12803  spwmo  14613  fbunfip  17854  usgranloopv  21351  usgraedg4  21359  usgraidx2vlem2  21364  usgrafisbase  21381  nbgra0nb  21394  nbgraf1olem3  21406  nbgraf1olem5  21408  nbcusgra  21425  cusgrasize2inds  21439  cusgrafi  21444  usgrasscusgra  21445  sizeusglecusglem1  21446  sizeusglecusg  21448  uvtxnbgra  21455  spthonepeq  21540  1pthoncl  21545  wlkdvspthlem  21560  cyclnspth  21571  fargshiftf1  21577  usgrcyclnl2  21581  nvnencycllem  21583  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  hashnbgravdg  21635  grpomndo  21887  rngoueqz  21971  zerdivemp1  21975  rngoridfz  21976  shmodsi  22844  kbass6  23577  mdsymlem6  23864  mdsymlem7  23865  cdj3lem2a  23892  cdj3lem3a  23895  predpo  25398  zerdivemp1x  26461  psgnunilem4  27288  funressnfv  27859  funbrafv  27889  otiunsndisj  27954  otiunsndisjX  27955  ssfz12  27976  elfzelfzelfz  27981  ubmelfzo  27986  ubmelm1fzo  27987  fzo1fzo0n0  27988  ssfzo12  27990  swrdnd  28001  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin12lem3a  28021  swrdccatin12lem3c  28023  swrdccatin12  28026  swrdccatin12b  28027  swrdccat3  28029  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspth  28038  usgra2pth  28041  usgra2adedgspthlem2  28044  el2wlkonotot0  28069  usg2wlkonot  28080  usg2wotspth  28081  usgfidegfi  28090  frgraunss  28099  frgra3vlem1  28104  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  4cycl2vnunb  28121  frgranbnb  28124  vdn0frgrav2  28128  vdn1frgrav2  28130  frgrancvvdeqlemB  28141  frgrawopreglem2  28148  frg2wot1  28160  usg2spot2nb  28168  2spotmdisj  28171  3imp31  28365  eel12131  28530  tratrbVD  28682  2uasbanhVD  28732  elpcliN  30375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator