MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com13 Structured version   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  1413  peano5  4868  funopg  5485  eldmrexrnb  5877  f1o2ndf1  6454  abianfp  6716  omordi  6809  omeulem1  6825  brecop  6997  isinf  7322  fiint  7383  carduni  7868  dfac5  8009  dfac2  8011  cofsmo  8149  cfcoflem  8152  domtriomlem  8322  axdc3lem2  8331  nqereu  8806  squeeze0  9913  zmax  10571  xrsupsslem  10885  xrinfmsslem  10886  supxrunb1  10898  supxrunb2  10899  difreicc  11028  elfznelfzo  11192  injresinjlem  11199  injresinj  11200  uzindi  11320  facwordi  11580  hasheqf1oi  11635  hashf1rn  11636  hash2prde  11688  sqr2irr  12848  spwmo  14658  bwth  17473  fbunfip  17901  usgranloopv  21398  usgraedg4  21406  usgraidx2vlem2  21411  usgrafisbase  21428  nbgra0nb  21441  nbgraf1olem3  21453  nbgraf1olem5  21455  nbcusgra  21472  cusgrasize2inds  21486  cusgrafi  21491  usgrasscusgra  21492  sizeusglecusglem1  21493  sizeusglecusg  21495  uvtxnbgra  21502  spthonepeq  21587  1pthoncl  21592  wlkdvspthlem  21607  cyclnspth  21618  fargshiftf1  21624  usgrcyclnl2  21628  nvnencycllem  21630  3v3e3cycl1  21631  4cycl4v4e  21653  4cycl4dv4e  21655  hashnbgravdg  21682  grpomndo  21934  rngoueqz  22018  zerdivemp1  22022  rngoridfz  22023  shmodsi  22891  kbass6  23624  mdsymlem6  23911  mdsymlem7  23912  cdj3lem2a  23939  cdj3lem3a  23942  predpo  25459  zerdivemp1x  26571  psgnunilem4  27397  funressnfv  27968  funbrafv  27998  otiunsndisj  28066  otiunsndisjX  28067  ssfz12  28104  elfzelfzelfz  28109  elfz0fzfz0  28114  fz0fzelfz0  28118  fz0fzdiffz0  28119  ubmelfzo  28126  ubmelm1fzo  28127  fzo1fzo0n0  28128  ssfzo12  28130  fzoopth  28139  swrdnd  28182  swrdvalodm2  28188  swrd0swrd  28197  swrdswrdlem  28198  swrdswrd  28199  swrdccatin1  28205  swrdccatin12lem3  28212  swrdccat  28216  2cshw1lem2  28249  2cshw  28256  2cshwmod  28257  cshweqdif2s  28271  cshweqrep  28274  cshwssizelem1a  28279  usg2wlkeq  28304  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspth  28308  usgra2pth  28311  usgra2adedgspthlem2  28314  el2wlkonotot0  28339  usg2wlkonot  28350  usg2wotspth  28351  usgfidegfi  28360  frgraunss  28385  frgra3vlem1  28390  3cyclfrgrarn1  28402  3cyclfrgrarn  28403  4cycl2vnunb  28407  frgranbnb  28410  vdn0frgrav2  28414  vdn1frgrav2  28416  frgrancvvdeqlemB  28427  frgrawopreglem2  28434  frg2wot1  28446  usg2spot2nb  28454  2spotmdisj  28457  3imp31  28654  eel12131  28821  tratrbVD  28973  2uasbanhVD  29023  elpcliN  30690
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator