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

Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3r 87	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com23 86	1 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

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  652  an31s  655  3imp31  1112  3imp21  1114  meredith  1643  preqsnd  4802  3elpr2eq  4849  propeqop  5461  po2ne  5555  funopg  6532  eldmrexrnb  7044  peano5  7844  f1o2ndf1  8072  suppimacnv  8124  omordi  8501  omeulem1  8517  brecop  8757  isinf  9175  fiint  9237  carduni  9905  dfac5  10051  dfac2b  10053  cofsmo  10191  cfcoflem  10194  domtriomlem  10364  axdc3lem2  10373  nqereu  10852  squeeze0  12059  zmax  12895  elpq  12925  xnn0lenn0nn0  13197  xrsupsslem  13259  xrinfmsslem  13260  supxrunb1  13271  supxrunb2  13272  difreicc  13437  elfz0ubfz0  13586  elfz0fzfz0  13587  fz0fzelfz0  13588  fz0fzdiffz0  13591  fzo1fzo0n0  13670  elfzodifsumelfzo  13686  ssfzo12  13714  ssfzo12bi  13716  fzoopth  13717  elfznelfzo  13728  injresinjlem  13745  injresinj  13746  addmodlteq  13908  uzindi  13944  ssnn0fi  13947  suppssfz  13956  facwordi  14251  hasheqf1oi  14313  hashf1rn  14314  fundmge2nop0  14464  swrdswrdlem  14666  swrdswrd  14667  wrd2ind  14685  swrdccatin1  14687  pfxccatin12lem2  14693  swrdccat  14697  reuccatpfxs1lem  14708  repsdf2  14740  cshwidx0  14768  cshweqrep  14783  2cshwcshw  14787  cshwcsh2id  14790  swrdco  14799  wwlktovfo  14920  sqrt2irr  16216  oddnn02np1  16317  oddge22np1  16318  evennn02n  16319  evennn2n  16320  dfgcd2  16515  lcmf  16602  lcmfunsnlem2lem2  16608  initoeu2lem1  17981  symgfix2  19391  gsmsymgreqlem2  19406  psgnunilem4  19472  01eq0ringOLD  20508  lmodfopnelem1  20893  nzerooringczr  21460  cply1mul  22261  gsummoncoe1  22273  mamufacex  22361  matecl  22390  gsummatr01  22624  mp2pm2mplem4  22774  chfacfscmul0  22823  chfacfpmmul0  22827  cayhamlem1  22831  fbunfip  23834  tngngp3  24621  mpomulcn  24834  zabsle1  27259  gausslemma2dlem1a  27328  2lgsoddprm  27379  2sqreunnltblem  27414  umgrnloopv  29175  upgredg2vtx  29210  usgruspgrb  29252  usgrnloopvALT  29270  usgredg2vlem2  29295  edg0usgr  29322  nbuhgr  29412  nbumgr  29416  nbuhgr2vtx1edgblem  29420  cusgredg  29493  cusgrsize2inds  29522  sizusglecusg  29532  umgr2v2enb1  29595  rusgr1vtx  29657  uspgr2wlkeq  29714  wlkreslem  29736  spthonepeq  29820  usgr2trlspth  29829  clwlkl1loop  29851  lfgrn1cycl  29873  uspgrn2crct  29876  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  wwlksnextbi  29962  wwlksnredwwlkn0  29964  wwlksnextinj  29967  wspthsnonn0vne  29985  umgr2adedgspth  30016  umgr2wlk  30017  usgr2wspthons3  30035  clwlkclwwlklem2a1  30062  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwwisshclwws  30085  erclwwlktr  30092  clwwlkn1loopb  30113  clwwlknwwlksnb  30125  clwwlkext2edg  30126  erclwwlkntr  30141  clwwlknon1  30167  clwwlknonwwlknonb  30176  clwwlknonex2lem2  30178  upgr1wlkdlem1  30215  upgr3v3e3cycl  30250  uhgr3cyclex  30252  upgr4cycl4dv4e  30255  eucrctshift  30313  frgr3vlem1  30343  3cyclfrgrrn1  30355  3cyclfrgrrn  30356  4cycl2vnunb  30360  frgrnbnb  30363  frgrncvvdeqlem8  30376  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  frgr2wwlk1  30399  2clwwlk2clwwlk  30420  numclwwlk1lem2fo  30428  frgrreg  30464  friendshipgt3  30468  shmodsi  31460  kbass6  32192  mdsymlem6  32479  mdsymlem7  32480  cdj3lem2a  32507  cdj3lem3a  32510  satfrel  35549  gonarlem  35576  satffunlem1lem1  35584  satffunlem2lem1  35586  satffun  35591  wl-spae  37846  grpomndo  38196  rngoueqz  38261  zerdivemp1x  38268  elpcliN  40339  dflim5  43757  relexpiidm  44131  relexpxpmin  44144  ntrk0kbimka  44466  eel12131  45139  tratrbVD  45287  2uasbanhVD  45337  funressnfv  47491  funbrafv  47606  otiunsndisjX  47727  ssfz12  47762  iccpartgt  47887  iccelpart  47893  iccpartnel  47898  fargshiftf1  47901  sprsymrelfvlem  47950  sprsymrelf1lem  47951  prproropf1olem4  47966  sbcpr  47981  reupr  47982  poprelb  47984  reuopreuprim  47986  fmtno4prmfac  48035  lighneallem4b  48072  lighneal  48074  nprmdvdsfacm1lem2  48084  mogoldbblem  48196  gbegt5  48237  sbgoldbaltlem1  48255  sbgoldbm  48260  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  grimedg  48411  cycl3grtri  48423  grlimgrtri  48479  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  lidldomn1  48707  2zrngamgm  48721  rngccatidALTV  48748  ringccatidALTV  48782  scmsuppss  48847  ply1mulgsumlem1  48862  lincsumcl  48907  ellcoellss  48911  lindslinindsimp1  48933  lindslinindimp2lem1  48934  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  itschlc0xyqsol1  49242