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  1111  3imp21  1113  meredith  1642  preqsnd  4810  3elpr2eq  4857  propeqop  5450  po2ne  5543  funopg  6520  eldmrexrnb  7031  peano5  7829  f1o2ndf1  8058  suppimacnv  8110  omordi  8487  omeulem1  8503  brecop  8740  isinf  9156  fiint  9218  carduni  9881  dfac5  10027  dfac2b  10029  cofsmo  10167  cfcoflem  10170  domtriomlem  10340  axdc3lem2  10349  nqereu  10827  squeeze0  12032  zmax  12845  elpq  12875  xnn0lenn0nn0  13146  xrsupsslem  13208  xrinfmsslem  13209  supxrunb1  13220  supxrunb2  13221  difreicc  13386  elfz0ubfz0  13534  elfz0fzfz0  13535  fz0fzelfz0  13536  fz0fzdiffz0  13539  fzo1fzo0n0  13617  elfzodifsumelfzo  13633  ssfzo12  13661  ssfzo12bi  13663  fzoopth  13664  elfznelfzo  13675  injresinjlem  13692  injresinj  13693  addmodlteq  13855  uzindi  13891  ssnn0fi  13894  suppssfz  13903  facwordi  14198  hasheqf1oi  14260  hashf1rn  14261  fundmge2nop0  14411  swrdswrdlem  14613  swrdswrd  14614  wrd2ind  14632  swrdccatin1  14634  pfxccatin12lem2  14640  swrdccat  14644  reuccatpfxs1lem  14655  repsdf2  14687  cshwidx0  14715  cshweqrep  14730  2cshwcshw  14734  cshwcsh2id  14737  swrdco  14746  wwlktovfo  14867  sqrt2irr  16160  oddnn02np1  16261  oddge22np1  16262  evennn02n  16263  evennn2n  16264  dfgcd2  16459  lcmf  16546  lcmfunsnlem2lem2  16552  initoeu2lem1  17923  symgfix2  19330  gsmsymgreqlem2  19345  psgnunilem4  19411  01eq0ringOLD  20448  lmodfopnelem1  20833  nzerooringczr  21419  cply1mul  22212  gsummoncoe1  22224  mamufacex  22312  matecl  22341  gsummatr01  22575  mp2pm2mplem4  22725  chfacfscmul0  22774  chfacfpmmul0  22778  cayhamlem1  22782  fbunfip  23785  tngngp3  24572  mpomulcn  24786  zabsle1  27235  gausslemma2dlem1a  27304  2lgsoddprm  27355  2sqreunnltblem  27390  umgrnloopv  29086  upgredg2vtx  29121  usgruspgrb  29163  usgrnloopvALT  29181  usgredg2vlem2  29206  edg0usgr  29233  nbuhgr  29323  nbumgr  29327  nbuhgr2vtx1edgblem  29331  cusgredg  29404  cusgrsize2inds  29434  sizusglecusg  29444  umgr2v2enb1  29507  rusgr1vtx  29569  uspgr2wlkeq  29626  wlkreslem  29648  spthonepeq  29732  usgr2trlspth  29741  clwlkl1loop  29763  lfgrn1cycl  29785  uspgrn2crct  29788  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  wwlksnextbi  29874  wwlksnredwwlkn0  29876  wwlksnextinj  29879  wspthsnonn0vne  29897  umgr2adedgspth  29928  umgr2wlk  29929  usgr2wspthons3  29947  clwlkclwwlklem2a1  29974  clwlkclwwlklem2fv2  29978  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwwisshclwws  29997  erclwwlktr  30004  clwwlkn1loopb  30025  clwwlknwwlksnb  30037  clwwlkext2edg  30038  erclwwlkntr  30053  clwwlknon1  30079  clwwlknonwwlknonb  30088  clwwlknonex2lem2  30090  upgr1wlkdlem1  30127  upgr3v3e3cycl  30162  uhgr3cyclex  30164  upgr4cycl4dv4e  30167  eucrctshift  30225  frgr3vlem1  30255  3cyclfrgrrn1  30267  3cyclfrgrrn  30268  4cycl2vnunb  30272  frgrnbnb  30275  frgrncvvdeqlem8  30288  frgrwopreglem5  30303  frgrwopreglem5ALT  30304  frgr2wwlk1  30311  2clwwlk2clwwlk  30332  numclwwlk1lem2fo  30340  frgrreg  30376  friendshipgt3  30380  shmodsi  31371  kbass6  32103  mdsymlem6  32390  mdsymlem7  32391  cdj3lem2a  32418  cdj3lem3a  32421  satfrel  35432  gonarlem  35459  satffunlem1lem1  35467  satffunlem2lem1  35469  satffun  35474  wl-spae  37586  grpomndo  37936  rngoueqz  38001  zerdivemp1x  38008  elpcliN  40013  dflim5  43447  relexpiidm  43822  relexpxpmin  43835  ntrk0kbimka  44157  eel12131  44830  tratrbVD  44978  2uasbanhVD  45028  funressnfv  47168  funbrafv  47283  otiunsndisjX  47404  ssfz12  47439  iccpartgt  47552  iccelpart  47558  iccpartnel  47563  fargshiftf1  47566  sprsymrelfvlem  47615  sprsymrelf1lem  47616  prproropf1olem4  47631  sbcpr  47646  reupr  47647  poprelb  47649  reuopreuprim  47651  fmtno4prmfac  47697  lighneallem4b  47734  lighneal  47736  mogoldbblem  47845  gbegt5  47886  sbgoldbaltlem1  47904  sbgoldbm  47909  bgoldbtbndlem2  47931  bgoldbtbndlem3  47932  bgoldbtbndlem4  47933  bgoldbtbnd  47934  grimedg  48060  cycl3grtri  48072  grlimgrtri  48128  pgnbgreunbgrlem2lem1  48239  pgnbgreunbgrlem2lem2  48240  pgnbgreunbgrlem2lem3  48241  lidldomn1  48356  2zrngamgm  48370  rngccatidALTV  48397  ringccatidALTV  48431  scmsuppss  48496  ply1mulgsumlem1  48512  lincsumcl  48557  ellcoellss  48561  lindslinindsimp1  48583  lindslinindimp2lem1  48584  nn0sumshdiglemA  48745  nn0sumshdiglemB  48746  itschlc0xyqsol1  48892