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  649  an31s  652  3imp31  1108  3imp21  1110  meredith  1642  preqsnd  4789  3elpr2eq  4837  propeqop  5397  po2ne  5489  predpo  6166  funopg  6389  eldmrexrnb  6858  fvn0fvelrn  6925  peano5  7605  f1o2ndf1  7818  suppimacnv  7841  omordi  8192  omeulem1  8208  brecop  8390  isinf  8731  fiint  8795  carduni  9410  dfac5  9554  dfac2b  9556  cofsmo  9691  cfcoflem  9694  domtriomlem  9864  axdc3lem2  9873  nqereu  10351  squeeze0  11543  zmax  12346  elpq  12375  xnn0lenn0nn0  12639  xrsupsslem  12701  xrinfmsslem  12702  supxrunb1  12713  supxrunb2  12714  difreicc  12871  elfz0ubfz0  13012  elfz0fzfz0  13013  fz0fzelfz0  13014  fz0fzdiffz0  13017  fzo1fzo0n0  13089  elfzodifsumelfzo  13104  ssfzo12  13131  ssfzo12bi  13133  elfznelfzo  13143  injresinjlem  13158  injresinj  13159  addmodlteq  13315  uzindi  13351  ssnn0fi  13354  suppssfz  13363  facwordi  13650  hasheqf1oi  13713  hashf1rn  13714  fundmge2nop0  13851  swrdswrdlem  14066  swrdswrd  14067  wrd2ind  14085  swrdccatin1  14087  pfxccatin12lem2  14093  swrdccat  14097  reuccatpfxs1lem  14108  repsdf2  14140  cshwidx0  14168  cshweqrep  14183  2cshwcshw  14187  cshwcsh2id  14190  swrdco  14199  wwlktovfo  14322  sqrt2irr  15602  oddnn02np1  15697  oddge22np1  15698  evennn02n  15699  evennn2n  15700  dfgcd2  15894  lcmf  15977  lcmfunsnlem2lem2  15983  initoeu2lem1  17274  symgfix2  18544  gsmsymgreqlem2  18559  psgnunilem4  18625  lmodfopnelem1  19670  01eq0ring  20045  cply1mul  20462  gsummoncoe1  20472  mamufacex  21000  matecl  21034  gsummatr01  21268  mp2pm2mplem4  21417  chfacfscmul0  21466  chfacfpmmul0  21470  cayhamlem1  21474  fbunfip  22477  tngngp3  23265  zabsle1  25872  gausslemma2dlem1a  25941  2lgsoddprm  25992  2sqreunnltblem  26027  umgrnloopv  26891  upgredg2vtx  26926  usgruspgrb  26966  usgrnloopvALT  26983  usgredg2vlem2  27008  edg0usgr  27035  nbuhgr  27125  nbumgr  27129  nbuhgr2vtx1edgblem  27133  cusgredg  27206  cusgrsize2inds  27235  sizusglecusg  27245  umgr2v2enb1  27308  rusgr1vtx  27370  uspgr2wlkeq  27427  wlkreslem  27451  spthonepeq  27533  usgr2trlspth  27542  clwlkl1loop  27564  lfgrn1cycl  27583  uspgrn2crct  27586  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  wwlksnextbi  27672  wwlksnredwwlkn0  27674  wwlksnextinj  27677  wspthsnonn0vne  27696  umgr2adedgspth  27727  umgr2wlk  27728  usgr2wspthons3  27743  clwlkclwwlklem2a1  27770  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwwisshclwws  27793  erclwwlktr  27800  clwwlkn1loopb  27821  clwwlknwwlksnb  27834  clwwlkext2edg  27835  erclwwlkntr  27850  clwwlknon1  27876  clwwlknonwwlknonb  27885  clwwlknonex2lem2  27887  upgr1wlkdlem1  27924  upgr3v3e3cycl  27959  uhgr3cyclex  27961  upgr4cycl4dv4e  27964  eucrctshift  28022  frgr3vlem1  28052  3cyclfrgrrn1  28064  3cyclfrgrrn  28065  4cycl2vnunb  28069  frgrnbnb  28072  frgrncvvdeqlem8  28085  frgrwopreglem5  28100  frgrwopreglem5ALT  28101  frgr2wwlk1  28108  2clwwlk2clwwlk  28129  numclwwlk1lem2fo  28137  frgrreg  28173  friendshipgt3  28177  shmodsi  29166  kbass6  29898  mdsymlem6  30185  mdsymlem7  30186  cdj3lem2a  30213  cdj3lem3a  30216  satfrel  32614  gonarlem  32641  satffunlem1lem1  32649  satffunlem2lem1  32651  satffun  32656  wl-spae  34776  grpomndo  35168  rngoueqz  35233  zerdivemp1x  35240  elpcliN  37044  relexpiidm  40098  relexpxpmin  40111  ntrk0kbimka  40438  eel12131  41096  tratrbVD  41244  2uasbanhVD  41294  funressnfv  43327  funbrafv  43406  otiunsndisjX  43527  ssfz12  43563  fzoopth  43576  iccpartgt  43636  iccelpart  43642  iccpartnel  43647  fargshiftf1  43650  sprsymrelfvlem  43701  sprsymrelf1lem  43702  prproropf1olem4  43717  sbcpr  43732  reupr  43733  poprelb  43735  reuopreuprim  43737  fmtno4prmfac  43783  lighneallem4b  43823  lighneal  43825  mogoldbblem  43934  gbegt5  43975  sbgoldbaltlem1  43993  sbgoldbm  43998  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  isomuspgrlem2b  44043  isomuspgrlem2d  44045  lidldomn1  44241  2zrngamgm  44259  rngccatidALTV  44309  ringccatidALTV  44372  nzerooringczr  44392  scmsuppss  44469  ply1mulgsumlem1  44489  lincsumcl  44535  ellcoellss  44539  lindslinindsimp1  44561  lindslinindimp2lem1  44562  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  itschlc0xyqsol1  44802