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  880  an31s  883  3imp31  1104  3imp21  1106  meredith  1715  preqsnd  4536  3elpr2eq  4587  propeqop  5118  predpo  5859  funopg  6083  eldmrexrnb  6530  fvn0fvelrn  6594  peano5  7255  f1o2ndf1  7454  suppimacnv  7475  omordi  7817  omeulem1  7833  brecop  8009  isinf  8340  fiint  8404  carduni  9017  dfac5  9161  dfac2b  9163  dfac2OLD  9165  cofsmo  9303  cfcoflem  9306  domtriomlem  9476  axdc3lem2  9485  nqereu  9963  squeeze0  11138  zmax  11998  xnn0lenn0nn0  12288  xrsupsslem  12350  xrinfmsslem  12351  supxrunb1  12362  supxrunb2  12363  difreicc  12517  elfz0ubfz0  12657  elfz0fzfz0  12658  fz0fzelfz0  12659  fz0fzdiffz0  12662  fzo1fzo0n0  12733  elfzodifsumelfzo  12748  ssfzo12  12775  ssfzo12bi  12777  elfznelfzo  12787  injresinjlem  12802  injresinj  12803  addmodlteq  12959  uzindi  12995  ssnn0fi  12998  suppssfz  13008  facwordi  13290  hasheqf1oi  13354  hashf1rn  13355  hash2prde  13464  fundmge2nop0  13486  swrdswrdlem  13679  swrdswrd  13680  wrd2ind  13697  reuccats1lem  13699  swrdccatin1  13703  swrdccatin12lem2  13709  swrdccat  13713  repsdf2  13745  cshwidx0  13772  cshweqrep  13787  2cshwcshw  13791  cshwcsh2id  13794  swrdco  13803  wwlktovfo  13922  sqrt2irr  15198  oddnn02np1  15294  oddge22np1  15295  evennn02n  15296  evennn2n  15297  dfgcd2  15485  lcmf  15568  lcmfunsnlem2lem2  15574  initoeu2lem1  16885  symgfix2  18056  gsmsymgreqlem2  18071  psgnunilem4  18137  lmodfopnelem1  19121  01eq0ring  19494  cply1mul  19886  gsummoncoe1  19896  mamufacex  20417  matecl  20453  gsummatr01lem4  20686  gsummatr01  20687  mp2pm2mplem4  20836  chfacfscmul0  20885  chfacfpmmul0  20889  cayhamlem1  20893  fbunfip  21894  tngngp3  22681  zabsle1  25241  gausslemma2dlem1a  25310  2lgsoddprm  25361  umgrnloopv  26221  upgredg2vtx  26256  usgruspgrb  26296  usgrnloopvALT  26313  usgredg2vlem2  26338  edg0usgr  26365  nbuhgr  26459  nbumgr  26463  nbuhgr2vtx1edgblem  26467  cusgredg  26551  cusgrsize2inds  26580  sizusglecusg  26590  umgr2v2enb1  26653  rusgr1vtx  26715  upgrewlkle2  26733  uspgr2wlkeq  26773  wlkreslem  26797  spthonepeq  26879  usgr2trlspth  26888  usgr2pth  26891  clwlkl1loop  26910  lfgrn1cycl  26929  uspgrn2crct  26932  crctcshwlkn0lem3  26936  crctcshwlkn0lem5  26938  wwlksnextbi  27033  wwlksnredwwlkn0  27035  wwlksnextinj  27038  wspthsnonn0vne  27058  umgr2adedgspth  27089  umgr2wlk  27090  usgr2wspthons3  27107  clwlkclwwlklem2a1  27136  clwlkclwwlklem2fv2  27140  clwlkclwwlklem2a4  27141  clwlkclwwlklem2a  27142  clwlkclwwlklem2  27144  clwwisshclwws  27159  erclwwlktr  27166  clwwlkn1loopb  27193  clwwlknwwlksnb  27206  clwwlkext2edg  27207  erclwwlkntr  27223  clwwlknon1  27266  clwwlknonwwlknonb  27275  clwwlknonwwlknonbOLD  27276  clwwlknonex2lem2  27278  upgr1wlkdlem1  27318  upgr3v3e3cycl  27353  uhgr3cyclex  27355  upgr4cycl4dv4e  27358  eucrctshift  27416  frgr3vlem1  27448  3cyclfrgrrn1  27460  3cyclfrgrrn  27461  4cycl2vnunb  27465  frgrnbnb  27468  frgrncvvdeqlem8  27481  frgrwopreglem5  27496  frgrwopreglem5ALT  27497  frgr2wwlk1  27504  2clwwlk2clwwlk  27528  numclwlk1lem2fo  27538  frgrreg  27583  friendshipgt3  27587  shmodsi  28578  kbass6  29310  mdsymlem6  29597  mdsymlem7  29598  cdj3lem2a  29625  cdj3lem3a  29628  bj-snmoore  33392  wl-spae  33637  grpomndo  34005  rngoueqz  34070  zerdivemp1x  34077  elpcliN  35700  relexpiidm  38516  relexpxpmin  38529  ntrk0kbimka  38857  eel12131  39458  tratrbVD  39614  2uasbanhVD  39664  funressnfv  41732  funbrafv  41762  otiunsndisjX  41824  ssfz12  41852  fzoopth  41865  iccpartgt  41891  iccelpart  41897  iccpartnel  41902  fargshiftf1  41905  pfxccatin12lem2  41952  reuccatpfxs1lem  41961  reuccatpfxs1  41962  fmtno4prmfac  42012  lighneallem4b  42054  lighneal  42056  mogoldbblem  42157  gbegt5  42177  sbgoldbaltlem1  42195  sbgoldbm  42200  bgoldbtbndlem2  42222  bgoldbtbndlem3  42223  bgoldbtbndlem4  42224  bgoldbtbnd  42225  sprsymrelfvlem  42268  sprsymrelf1lem  42269  lidldomn1  42449  2zrngamgm  42467  rngccatidALTV  42517  ringccatidALTV  42580  nzerooringczr  42600  scmsuppss  42681  ply1mulgsumlem1  42702  lincsumcl  42748  ellcoellss  42752  lindslinindsimp1  42774  lindslinindimp2lem1  42775  nn0sumshdiglemA  42941  nn0sumshdiglemB  42942
  Copyright terms: Public domain W3C validator