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  4817  3elpr2eq  4864  propeqop  5463  po2ne  5556  funopg  6534  eldmrexrnb  7046  peano5  7845  f1o2ndf1  8074  suppimacnv  8126  omordi  8503  omeulem1  8519  brecop  8759  isinf  9177  fiint  9239  carduni  9905  dfac5  10051  dfac2b  10053  cofsmo  10191  cfcoflem  10194  domtriomlem  10364  axdc3lem2  10373  nqereu  10852  squeeze0  12057  zmax  12870  elpq  12900  xnn0lenn0nn0  13172  xrsupsslem  13234  xrinfmsslem  13235  supxrunb1  13246  supxrunb2  13247  difreicc  13412  elfz0ubfz0  13560  elfz0fzfz0  13561  fz0fzelfz0  13562  fz0fzdiffz0  13565  fzo1fzo0n0  13643  elfzodifsumelfzo  13659  ssfzo12  13687  ssfzo12bi  13689  fzoopth  13690  elfznelfzo  13701  injresinjlem  13718  injresinj  13719  addmodlteq  13881  uzindi  13917  ssnn0fi  13920  suppssfz  13929  facwordi  14224  hasheqf1oi  14286  hashf1rn  14287  fundmge2nop0  14437  swrdswrdlem  14639  swrdswrd  14640  wrd2ind  14658  swrdccatin1  14660  pfxccatin12lem2  14666  swrdccat  14670  reuccatpfxs1lem  14681  repsdf2  14713  cshwidx0  14741  cshweqrep  14756  2cshwcshw  14760  cshwcsh2id  14763  swrdco  14772  wwlktovfo  14893  sqrt2irr  16186  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  dfgcd2  16485  lcmf  16572  lcmfunsnlem2lem2  16578  initoeu2lem1  17950  symgfix2  19357  gsmsymgreqlem2  19372  psgnunilem4  19438  01eq0ringOLD  20476  lmodfopnelem1  20861  nzerooringczr  21447  cply1mul  22252  gsummoncoe1  22264  mamufacex  22352  matecl  22381  gsummatr01  22615  mp2pm2mplem4  22765  chfacfscmul0  22814  chfacfpmmul0  22818  cayhamlem1  22822  fbunfip  23825  tngngp3  24612  mpomulcn  24826  zabsle1  27275  gausslemma2dlem1a  27344  2lgsoddprm  27395  2sqreunnltblem  27430  umgrnloopv  29191  upgredg2vtx  29226  usgruspgrb  29268  usgrnloopvALT  29286  usgredg2vlem2  29311  edg0usgr  29338  nbuhgr  29428  nbumgr  29432  nbuhgr2vtx1edgblem  29436  cusgredg  29509  cusgrsize2inds  29539  sizusglecusg  29549  umgr2v2enb1  29612  rusgr1vtx  29674  uspgr2wlkeq  29731  wlkreslem  29753  spthonepeq  29837  usgr2trlspth  29846  clwlkl1loop  29868  lfgrn1cycl  29890  uspgrn2crct  29893  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  wwlksnextbi  29979  wwlksnredwwlkn0  29981  wwlksnextinj  29984  wspthsnonn0vne  30002  umgr2adedgspth  30033  umgr2wlk  30034  usgr2wspthons3  30052  clwlkclwwlklem2a1  30079  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwwisshclwws  30102  erclwwlktr  30109  clwwlkn1loopb  30130  clwwlknwwlksnb  30142  clwwlkext2edg  30143  erclwwlkntr  30158  clwwlknon1  30184  clwwlknonwwlknonb  30193  clwwlknonex2lem2  30195  upgr1wlkdlem1  30232  upgr3v3e3cycl  30267  uhgr3cyclex  30269  upgr4cycl4dv4e  30272  eucrctshift  30330  frgr3vlem1  30360  3cyclfrgrrn1  30372  3cyclfrgrrn  30373  4cycl2vnunb  30377  frgrnbnb  30380  frgrncvvdeqlem8  30393  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  frgr2wwlk1  30416  2clwwlk2clwwlk  30437  numclwwlk1lem2fo  30445  frgrreg  30481  friendshipgt3  30485  shmodsi  31476  kbass6  32208  mdsymlem6  32495  mdsymlem7  32496  cdj3lem2a  32523  cdj3lem3a  32526  satfrel  35580  gonarlem  35607  satffunlem1lem1  35615  satffunlem2lem1  35617  satffun  35622  wl-spae  37773  grpomndo  38123  rngoueqz  38188  zerdivemp1x  38195  elpcliN  40266  dflim5  43683  relexpiidm  44057  relexpxpmin  44070  ntrk0kbimka  44392  eel12131  45065  tratrbVD  45213  2uasbanhVD  45263  funressnfv  47400  funbrafv  47515  otiunsndisjX  47636  ssfz12  47671  iccpartgt  47784  iccelpart  47790  iccpartnel  47795  fargshiftf1  47798  sprsymrelfvlem  47847  sprsymrelf1lem  47848  prproropf1olem4  47863  sbcpr  47878  reupr  47879  poprelb  47881  reuopreuprim  47883  fmtno4prmfac  47929  lighneallem4b  47966  lighneal  47968  mogoldbblem  48077  gbegt5  48118  sbgoldbaltlem1  48136  sbgoldbm  48141  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  bgoldbtbndlem4  48165  bgoldbtbnd  48166  grimedg  48292  cycl3grtri  48304  grlimgrtri  48360  pgnbgreunbgrlem2lem1  48471  pgnbgreunbgrlem2lem2  48472  pgnbgreunbgrlem2lem3  48473  lidldomn1  48588  2zrngamgm  48602  rngccatidALTV  48629  ringccatidALTV  48663  scmsuppss  48728  ply1mulgsumlem1  48743  lincsumcl  48788  ellcoellss  48792  lindslinindsimp1  48814  lindslinindimp2lem1  48815  nn0sumshdiglemA  48976  nn0sumshdiglemB  48977  itschlc0xyqsol1  49123