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  imim12  105  an13s  844  an31s  847  3imp31  1255  meredith  1563  propeqop  4940  predpo  5667  funopg  5890  eldmrexrnb  6332  fvn0fvelrn  6395  peano5  7051  f1o2ndf1  7245  suppimacnv  7266  omordi  7606  omeulem1  7622  brecop  7800  isinf  8133  fiint  8197  carduni  8767  dfac5  8911  dfac2  8913  cofsmo  9051  cfcoflem  9054  domtriomlem  9224  axdc3lem2  9233  nqereu  9711  squeeze0  10886  zmax  11745  xnn0lenn0nn0  12034  xrsupsslem  12096  xrinfmsslem  12097  supxrunb1  12108  supxrunb2  12109  difreicc  12262  elfz0ubfz0  12400  elfz0fzfz0  12401  fz0fzelfz0  12402  fz0fzdiffz0  12405  fzo1fzo0n0  12475  elfzodifsumelfzo  12490  ssfzo12  12518  ssfzo12bi  12520  elfznelfzo  12530  injresinjlem  12544  injresinj  12545  addmodlteq  12701  uzindi  12737  ssnn0fi  12740  suppssfz  12750  facwordi  13032  hasheqf1oi  13096  hasheqf1oiOLD  13097  hashf1rn  13098  hashf1rnOLD  13099  hash2prde  13206  fundmge2nop0  13229  swrdswrdlem  13413  swrdswrd  13414  wrd2ind  13431  reuccats1lem  13433  swrdccatin1  13436  swrdccatin12lem2  13442  swrdccat  13446  repsdf2  13478  cshwidx0  13505  cshweqrep  13520  2cshwcshw  13524  cshwcsh2id  13527  swrdco  13536  wwlktovfo  13651  sqrt2irr  14922  oddnn02np1  15015  oddge22np1  15016  evennn02n  15017  evennn2n  15018  dfgcd2  15206  lcmf  15289  lcmfunsnlem2lem2  15295  initoeu2lem1  16604  symgfix2  17776  gsmsymgreqlem2  17791  psgnunilem4  17857  lmodfopnelem1  18839  01eq0ring  19212  cply1mul  19604  gsummoncoe1  19614  mamufacex  20135  matecl  20171  gsummatr01lem4  20404  gsummatr01  20405  mp2pm2mplem4  20554  chfacfscmul0  20603  chfacfpmmul0  20607  cayhamlem1  20611  fbunfip  21613  tngngp3  22400  zabsle1  24955  gausslemma2dlem1a  25024  2lgsoddprm  25075  umgrnloopv  25930  upgredg2vtx  25965  usgruspgrb  26003  usgrnloopvALT  26020  usgredg2vlem2  26045  edg0usgr  26072  nbuhgr  26160  nbumgr  26164  nbuhgr2vtx1edgblem  26168  cusgredg  26241  cusgrsize2inds  26270  sizusglecusg  26280  umgr2v2enb1  26342  rusgr1vtx  26388  upgrewlkle2  26406  uspgr2wlkeq  26445  wlkreslem  26469  spthonepeq  26551  usgr2trlspth  26560  usgr2pth  26563  clwlkl1loop  26581  lfgrn1cycl  26600  uspgrn2crct  26603  crctcshwlkn0lem3  26607  crctcshwlkn0lem5  26609  wwlksnextbi  26692  wwlksnredwwlkn0  26694  wwlksnextinj  26697  wspthsnonn0vne  26716  umgr2adedgspth  26747  umgr2wlk  26748  usgr2wspthons3  26759  clwlkclwwlklem2a1  26794  clwlkclwwlklem2fv2  26798  clwlkclwwlklem2a4  26799  clwlkclwwlklem2a  26800  clwlkclwwlklem2  26802  clwwlksext2edg  26823  clwwisshclwws  26828  erclwwlkstr  26836  erclwwlksntr  26848  upgr1wlkdlem1  26905  upgr3v3e3cycl  26940  uhgr3cyclex  26942  upgr4cycl4dv4e  26945  eucrctshift  27003  frgr3vlem1  27035  3cyclfrgrrn1  27047  3cyclfrgrrn  27048  4cycl2vnunb  27052  frgrnbnb  27055  frgrncvvdeqlemB  27069  frgr2wwlk1  27086  numclwwlkffin0  27105  numclwlk1lem2fo  27117  frgrreg  27140  friendshipgt3  27144  shmodsi  28136  kbass6  28868  mdsymlem6  29155  mdsymlem7  29156  cdj3lem2a  29183  cdj3lem3a  29186  wl-spae  32977  grpomndo  33345  rngoueqz  33410  zerdivemp1x  33417  elpcliN  34698  relexpiidm  37516  relexpxpmin  37529  ntrk0kbimka  37858  eel12131  38459  tratrbVD  38619  2uasbanhVD  38669  funressnfv  40542  funbrafv  40572  otiunsndisjX  40625  ssfz12  40651  fzoopth  40664  iccpartgt  40691  iccelpart  40697  iccpartnel  40702  fargshiftf1  40705  pfxccatin12lem2  40753  reuccatpfxs1lem  40762  reuccatpfxs1  40763  fmtno4prmfac  40813  lighneallem4b  40855  lighneal  40857  gbegt5  40974  sgoldbaltlem1  40992  bgoldbtbndlem2  41013  bgoldbtbndlem3  41014  bgoldbtbndlem4  41015  bgoldbtbnd  41016  sprsymrelfvlem  41058  sprsymrelf1lem  41059  lidldomn1  41239  2zrngamgm  41257  rngccatidALTV  41307  ringccatidALTV  41370  nzerooringczr  41390  scmsuppss  41471  ply1mulgsumlem1  41492  lincsumcl  41538  ellcoellss  41542  lindslinindsimp1  41564  lindslinindimp2lem1  41565  nn0sumshdiglemA  41735  nn0sumshdiglemB  41736
  Copyright terms: Public domain W3C validator