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

Theorem com13 88
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 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com13 (𝜒 → (𝜓 → (𝜑𝜃)))

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3r 87 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 86 1 (𝜒 → (𝜓 → (𝜑𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com24  95  an13s  650  an31s  653  3imp31  1113  3imp21  1115  meredith  1644  preqsnd  4817  3elpr2eq  4865  propeqop  5465  po2ne  5562  funopg  6536  eldmrexrnb  7043  fvn0fvelrnOLD  7110  peano5  7831  peano5OLD  7832  f1o2ndf1  8055  suppimacnv  8106  omordi  8514  omeulem1  8530  brecop  8752  isinf  9207  isinfOLD  9208  fiint  9271  carduni  9922  dfac5  10069  dfac2b  10071  cofsmo  10210  cfcoflem  10213  domtriomlem  10383  axdc3lem2  10392  nqereu  10870  squeeze0  12063  zmax  12875  elpq  12905  xnn0lenn0nn0  13170  xrsupsslem  13232  xrinfmsslem  13233  supxrunb1  13244  supxrunb2  13245  difreicc  13407  elfz0ubfz0  13551  elfz0fzfz0  13552  fz0fzelfz0  13553  fz0fzdiffz0  13556  fzo1fzo0n0  13629  elfzodifsumelfzo  13644  ssfzo12  13671  ssfzo12bi  13673  elfznelfzo  13683  injresinjlem  13698  injresinj  13699  addmodlteq  13857  uzindi  13893  ssnn0fi  13896  suppssfz  13905  facwordi  14195  hasheqf1oi  14257  hashf1rn  14258  fundmge2nop0  14397  swrdswrdlem  14598  swrdswrd  14599  wrd2ind  14617  swrdccatin1  14619  pfxccatin12lem2  14625  swrdccat  14629  reuccatpfxs1lem  14640  repsdf2  14672  cshwidx0  14700  cshweqrep  14715  2cshwcshw  14720  cshwcsh2id  14723  swrdco  14732  wwlktovfo  14853  sqrt2irr  16136  oddnn02np1  16235  oddge22np1  16236  evennn02n  16237  evennn2n  16238  dfgcd2  16432  lcmf  16514  lcmfunsnlem2lem2  16520  initoeu2lem1  17905  symgfix2  19203  gsmsymgreqlem2  19218  psgnunilem4  19284  lmodfopnelem1  20373  01eq0ring  20758  cply1mul  21681  gsummoncoe1  21691  mamufacex  21754  matecl  21790  gsummatr01  22024  mp2pm2mplem4  22174  chfacfscmul0  22223  chfacfpmmul0  22227  cayhamlem1  22231  fbunfip  23236  tngngp3  24036  zabsle1  26660  gausslemma2dlem1a  26729  2lgsoddprm  26780  2sqreunnltblem  26815  umgrnloopv  28099  upgredg2vtx  28134  usgruspgrb  28174  usgrnloopvALT  28191  usgredg2vlem2  28216  edg0usgr  28243  nbuhgr  28333  nbumgr  28337  nbuhgr2vtx1edgblem  28341  cusgredg  28414  cusgrsize2inds  28443  sizusglecusg  28453  umgr2v2enb1  28516  rusgr1vtx  28578  uspgr2wlkeq  28636  wlkreslem  28659  spthonepeq  28742  usgr2trlspth  28751  clwlkl1loop  28773  lfgrn1cycl  28792  uspgrn2crct  28795  crctcshwlkn0lem3  28799  crctcshwlkn0lem5  28801  wwlksnextbi  28881  wwlksnredwwlkn0  28883  wwlksnextinj  28886  wspthsnonn0vne  28904  umgr2adedgspth  28935  umgr2wlk  28936  usgr2wspthons3  28951  clwlkclwwlklem2a1  28978  clwlkclwwlklem2fv2  28982  clwlkclwwlklem2a4  28983  clwlkclwwlklem2a  28984  clwlkclwwlklem2  28986  clwwisshclwws  29001  erclwwlktr  29008  clwwlkn1loopb  29029  clwwlknwwlksnb  29041  clwwlkext2edg  29042  erclwwlkntr  29057  clwwlknon1  29083  clwwlknonwwlknonb  29092  clwwlknonex2lem2  29094  upgr1wlkdlem1  29131  upgr3v3e3cycl  29166  uhgr3cyclex  29168  upgr4cycl4dv4e  29171  eucrctshift  29229  frgr3vlem1  29259  3cyclfrgrrn1  29271  3cyclfrgrrn  29272  4cycl2vnunb  29276  frgrnbnb  29279  frgrncvvdeqlem8  29292  frgrwopreglem5  29307  frgrwopreglem5ALT  29308  frgr2wwlk1  29315  2clwwlk2clwwlk  29336  numclwwlk1lem2fo  29344  frgrreg  29380  friendshipgt3  29384  shmodsi  30373  kbass6  31105  mdsymlem6  31392  mdsymlem7  31393  cdj3lem2a  31420  cdj3lem3a  31423  satfrel  34018  gonarlem  34045  satffunlem1lem1  34053  satffunlem2lem1  34055  satffun  34060  wl-spae  36026  grpomndo  36380  rngoueqz  36445  zerdivemp1x  36452  elpcliN  38402  dflim5  41707  relexpiidm  42064  relexpxpmin  42077  ntrk0kbimka  42399  eel12131  43083  tratrbVD  43231  2uasbanhVD  43281  funressnfv  45363  funbrafv  45476  otiunsndisjX  45597  ssfz12  45632  fzoopth  45645  iccpartgt  45705  iccelpart  45711  iccpartnel  45716  fargshiftf1  45719  sprsymrelfvlem  45768  sprsymrelf1lem  45769  prproropf1olem4  45784  sbcpr  45799  reupr  45800  poprelb  45802  reuopreuprim  45804  fmtno4prmfac  45850  lighneallem4b  45887  lighneal  45889  mogoldbblem  45998  gbegt5  46039  sbgoldbaltlem1  46057  sbgoldbm  46062  bgoldbtbndlem2  46084  bgoldbtbndlem3  46085  bgoldbtbndlem4  46086  bgoldbtbnd  46087  isomuspgrlem2b  46107  isomuspgrlem2d  46109  lidldomn1  46305  2zrngamgm  46323  rngccatidALTV  46373  ringccatidALTV  46436  nzerooringczr  46456  scmsuppss  46534  ply1mulgsumlem1  46553  lincsumcl  46598  ellcoellss  46602  lindslinindsimp1  46624  lindslinindimp2lem1  46625  nn0sumshdiglemA  46791  nn0sumshdiglemB  46792  itschlc0xyqsol1  46938
  Copyright terms: Public domain W3C validator