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  651  an31s  654  3imp31  1112  3imp21  1114  meredith  1641  preqsnd  4859  3elpr2eq  4906  propeqop  5512  po2ne  5608  funopg  6600  eldmrexrnb  7112  fvn0fvelrnOLD  7183  peano5  7915  f1o2ndf1  8147  suppimacnv  8199  omordi  8604  omeulem1  8620  brecop  8850  isinf  9296  isinfOLD  9297  fiint  9366  fiintOLD  9367  carduni  10021  dfac5  10169  dfac2b  10171  cofsmo  10309  cfcoflem  10312  domtriomlem  10482  axdc3lem2  10491  nqereu  10969  squeeze0  12171  zmax  12987  elpq  13017  xnn0lenn0nn0  13287  xrsupsslem  13349  xrinfmsslem  13350  supxrunb1  13361  supxrunb2  13362  difreicc  13524  elfz0ubfz0  13672  elfz0fzfz0  13673  fz0fzelfz0  13674  fz0fzdiffz0  13677  fzo1fzo0n0  13754  elfzodifsumelfzo  13770  ssfzo12  13798  ssfzo12bi  13800  fzoopth  13801  elfznelfzo  13811  injresinjlem  13826  injresinj  13827  addmodlteq  13987  uzindi  14023  ssnn0fi  14026  suppssfz  14035  facwordi  14328  hasheqf1oi  14390  hashf1rn  14391  fundmge2nop0  14541  swrdswrdlem  14742  swrdswrd  14743  wrd2ind  14761  swrdccatin1  14763  pfxccatin12lem2  14769  swrdccat  14773  reuccatpfxs1lem  14784  repsdf2  14816  cshwidx0  14844  cshweqrep  14859  2cshwcshw  14864  cshwcsh2id  14867  swrdco  14876  wwlktovfo  14997  sqrt2irr  16285  oddnn02np1  16385  oddge22np1  16386  evennn02n  16387  evennn2n  16388  dfgcd2  16583  lcmf  16670  lcmfunsnlem2lem2  16676  initoeu2lem1  18059  symgfix2  19434  gsmsymgreqlem2  19449  psgnunilem4  19515  01eq0ringOLD  20531  lmodfopnelem1  20896  nzerooringczr  21491  cply1mul  22300  gsummoncoe1  22312  mamufacex  22400  matecl  22431  gsummatr01  22665  mp2pm2mplem4  22815  chfacfscmul0  22864  chfacfpmmul0  22868  cayhamlem1  22872  fbunfip  23877  tngngp3  24677  mpomulcn  24891  zabsle1  27340  gausslemma2dlem1a  27409  2lgsoddprm  27460  2sqreunnltblem  27495  umgrnloopv  29123  upgredg2vtx  29158  usgruspgrb  29200  usgrnloopvALT  29218  usgredg2vlem2  29243  edg0usgr  29270  nbuhgr  29360  nbumgr  29364  nbuhgr2vtx1edgblem  29368  cusgredg  29441  cusgrsize2inds  29471  sizusglecusg  29481  umgr2v2enb1  29544  rusgr1vtx  29606  uspgr2wlkeq  29664  wlkreslem  29687  spthonepeq  29772  usgr2trlspth  29781  clwlkl1loop  29803  lfgrn1cycl  29825  uspgrn2crct  29828  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  wwlksnextbi  29914  wwlksnredwwlkn0  29916  wwlksnextinj  29919  wspthsnonn0vne  29937  umgr2adedgspth  29968  umgr2wlk  29969  usgr2wspthons3  29984  clwlkclwwlklem2a1  30011  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwwisshclwws  30034  erclwwlktr  30041  clwwlkn1loopb  30062  clwwlknwwlksnb  30074  clwwlkext2edg  30075  erclwwlkntr  30090  clwwlknon1  30116  clwwlknonwwlknonb  30125  clwwlknonex2lem2  30127  upgr1wlkdlem1  30164  upgr3v3e3cycl  30199  uhgr3cyclex  30201  upgr4cycl4dv4e  30204  eucrctshift  30262  frgr3vlem1  30292  3cyclfrgrrn1  30304  3cyclfrgrrn  30305  4cycl2vnunb  30309  frgrnbnb  30312  frgrncvvdeqlem8  30325  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  frgr2wwlk1  30348  2clwwlk2clwwlk  30369  numclwwlk1lem2fo  30377  frgrreg  30413  friendshipgt3  30417  shmodsi  31408  kbass6  32140  mdsymlem6  32427  mdsymlem7  32428  cdj3lem2a  32455  cdj3lem3a  32458  satfrel  35372  gonarlem  35399  satffunlem1lem1  35407  satffunlem2lem1  35409  satffun  35414  wl-spae  37522  grpomndo  37882  rngoueqz  37947  zerdivemp1x  37954  elpcliN  39895  dflim5  43342  relexpiidm  43717  relexpxpmin  43730  ntrk0kbimka  44052  eel12131  44733  tratrbVD  44881  2uasbanhVD  44931  funressnfv  47055  funbrafv  47170  otiunsndisjX  47291  ssfz12  47326  iccpartgt  47414  iccelpart  47420  iccpartnel  47425  fargshiftf1  47428  sprsymrelfvlem  47477  sprsymrelf1lem  47478  prproropf1olem4  47493  sbcpr  47508  reupr  47509  poprelb  47511  reuopreuprim  47513  fmtno4prmfac  47559  lighneallem4b  47596  lighneal  47598  mogoldbblem  47707  gbegt5  47748  sbgoldbaltlem1  47766  sbgoldbm  47771  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  grimedg  47903  cycl3grtri  47914  grlimgrtri  47963  lidldomn1  48147  2zrngamgm  48161  rngccatidALTV  48188  ringccatidALTV  48222  scmsuppss  48287  ply1mulgsumlem1  48303  lincsumcl  48348  ellcoellss  48352  lindslinindsimp1  48374  lindslinindimp2lem1  48375  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  itschlc0xyqsol1  48687