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  862  an31s  865  3imp31  1276  meredith  1606  3elpr2eq  4467  propeqop  4999  predpo  5736  funopg  5960  eldmrexrnb  6406  fvn0fvelrn  6470  peano5  7131  f1o2ndf1  7330  suppimacnv  7351  omordi  7691  omeulem1  7707  brecop  7883  isinf  8214  fiint  8278  carduni  8845  dfac5  8989  dfac2  8991  cofsmo  9129  cfcoflem  9132  domtriomlem  9302  axdc3lem2  9311  nqereu  9789  squeeze0  10964  zmax  11823  xnn0lenn0nn0  12113  xrsupsslem  12175  xrinfmsslem  12176  supxrunb1  12187  supxrunb2  12188  difreicc  12342  elfz0ubfz0  12482  elfz0fzfz0  12483  fz0fzelfz0  12484  fz0fzdiffz0  12487  fzo1fzo0n0  12558  elfzodifsumelfzo  12573  ssfzo12  12601  ssfzo12bi  12603  elfznelfzo  12613  injresinjlem  12628  injresinj  12629  addmodlteq  12785  uzindi  12821  ssnn0fi  12824  suppssfz  12834  facwordi  13116  hasheqf1oi  13180  hashf1rn  13181  hash2prde  13290  fundmge2nop0  13312  swrdswrdlem  13505  swrdswrd  13506  wrd2ind  13523  reuccats1lem  13525  swrdccatin1  13529  swrdccatin12lem2  13535  swrdccat  13539  repsdf2  13571  cshwidx0  13598  cshweqrep  13613  2cshwcshw  13617  cshwcsh2id  13620  swrdco  13629  wwlktovfo  13747  sqrt2irr  15023  oddnn02np1  15119  oddge22np1  15120  evennn02n  15121  evennn2n  15122  dfgcd2  15310  lcmf  15393  lcmfunsnlem2lem2  15399  initoeu2lem1  16711  symgfix2  17882  gsmsymgreqlem2  17897  psgnunilem4  17963  lmodfopnelem1  18947  01eq0ring  19320  cply1mul  19712  gsummoncoe1  19722  mamufacex  20243  matecl  20279  gsummatr01lem4  20512  gsummatr01  20513  mp2pm2mplem4  20662  chfacfscmul0  20711  chfacfpmmul0  20715  cayhamlem1  20719  fbunfip  21720  tngngp3  22507  zabsle1  25066  gausslemma2dlem1a  25135  2lgsoddprm  25186  umgrnloopv  26046  upgredg2vtx  26081  usgruspgrb  26121  usgrnloopvALT  26138  usgredg2vlem2  26163  edg0usgr  26190  nbuhgr  26284  nbumgr  26288  nbuhgr2vtx1edgblem  26292  cusgredg  26376  cusgrsize2inds  26405  sizusglecusg  26415  umgr2v2enb1  26478  rusgr1vtx  26540  upgrewlkle2  26558  uspgr2wlkeq  26598  wlkreslem  26622  spthonepeq  26704  usgr2trlspth  26713  usgr2pth  26716  clwlkl1loop  26734  lfgrn1cycl  26753  uspgrn2crct  26756  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  wwlksnextbi  26857  wwlksnredwwlkn0  26859  wwlksnextinj  26862  wspthsnonn0vne  26882  umgr2adedgspth  26913  umgr2wlk  26914  usgr2wspthons3  26931  clwlkclwwlklem2a1  26958  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwwisshclwws  26972  erclwwlktr  26979  clwwlkn1loopb  27006  clwwlknwwlksnb  27019  clwwlkext2edg  27020  erclwwlkntr  27035  clwwlknon1  27072  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  clwwlknonex2lem2  27083  upgr1wlkdlem1  27123  upgr3v3e3cycl  27158  uhgr3cyclex  27160  upgr4cycl4dv4e  27163  eucrctshift  27221  frgr3vlem1  27253  3cyclfrgrrn1  27265  3cyclfrgrrn  27266  4cycl2vnunb  27270  frgrnbnb  27273  frgrncvvdeqlem8  27286  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  frgr2wwlk1  27309  2clwwlk2clwwlk  27338  numclwlk1lem2fo  27348  frgrreg  27381  friendshipgt3  27385  shmodsi  28376  kbass6  29108  mdsymlem6  29395  mdsymlem7  29396  cdj3lem2a  29423  cdj3lem3a  29426  bj-snmoore  33193  wl-spae  33436  grpomndo  33804  rngoueqz  33869  zerdivemp1x  33876  elpcliN  35497  relexpiidm  38313  relexpxpmin  38326  ntrk0kbimka  38654  eel12131  39255  tratrbVD  39411  2uasbanhVD  39461  funressnfv  41529  funbrafv  41559  otiunsndisjX  41621  ssfz12  41649  fzoopth  41662  iccpartgt  41688  iccelpart  41694  iccpartnel  41699  fargshiftf1  41702  pfxccatin12lem2  41749  reuccatpfxs1lem  41758  reuccatpfxs1  41759  fmtno4prmfac  41809  lighneallem4b  41851  lighneal  41853  mogoldbblem  41954  gbegt5  41974  sbgoldbaltlem1  41992  sbgoldbm  41997  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  bgoldbtbnd  42022  sprsymrelfvlem  42065  sprsymrelf1lem  42066  lidldomn1  42246  2zrngamgm  42264  rngccatidALTV  42314  ringccatidALTV  42377  nzerooringczr  42397  scmsuppss  42478  ply1mulgsumlem1  42499  lincsumcl  42545  ellcoellss  42549  lindslinindsimp1  42571  lindslinindimp2lem1  42572  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator