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  648  an31s  651  3imp31  1111  3imp21  1113  meredith  1642  preqsnd  4802  3elpr2eq  4850  propeqop  5445  po2ne  5542  funopg  6512  eldmrexrnb  7018  fvn0fvelrnOLD  7085  peano5  7800  peano5OLD  7801  f1o2ndf1  8022  suppimacnv  8052  omordi  8460  omeulem1  8476  brecop  8662  isinf  9117  isinfOLD  9118  fiint  9181  carduni  9830  dfac5  9977  dfac2b  9979  cofsmo  10118  cfcoflem  10121  domtriomlem  10291  axdc3lem2  10300  nqereu  10778  squeeze0  11971  zmax  12778  elpq  12808  xnn0lenn0nn0  13072  xrsupsslem  13134  xrinfmsslem  13135  supxrunb1  13146  supxrunb2  13147  difreicc  13309  elfz0ubfz0  13453  elfz0fzfz0  13454  fz0fzelfz0  13455  fz0fzdiffz0  13458  fzo1fzo0n0  13531  elfzodifsumelfzo  13546  ssfzo12  13573  ssfzo12bi  13575  elfznelfzo  13585  injresinjlem  13600  injresinj  13601  addmodlteq  13759  uzindi  13795  ssnn0fi  13798  suppssfz  13807  facwordi  14096  hasheqf1oi  14158  hashf1rn  14159  fundmge2nop0  14298  swrdswrdlem  14507  swrdswrd  14508  wrd2ind  14526  swrdccatin1  14528  pfxccatin12lem2  14534  swrdccat  14538  reuccatpfxs1lem  14549  repsdf2  14581  cshwidx0  14609  cshweqrep  14624  2cshwcshw  14629  cshwcsh2id  14632  swrdco  14641  wwlktovfo  14764  sqrt2irr  16049  oddnn02np1  16148  oddge22np1  16149  evennn02n  16150  evennn2n  16151  dfgcd2  16345  lcmf  16427  lcmfunsnlem2lem2  16433  initoeu2lem1  17818  symgfix2  19112  gsmsymgreqlem2  19127  psgnunilem4  19193  lmodfopnelem1  20257  01eq0ring  20641  cply1mul  21563  gsummoncoe1  21573  mamufacex  21636  matecl  21672  gsummatr01  21906  mp2pm2mplem4  22056  chfacfscmul0  22105  chfacfpmmul0  22109  cayhamlem1  22113  fbunfip  23118  tngngp3  23918  zabsle1  26542  gausslemma2dlem1a  26611  2lgsoddprm  26662  2sqreunnltblem  26697  umgrnloopv  27678  upgredg2vtx  27713  usgruspgrb  27753  usgrnloopvALT  27770  usgredg2vlem2  27795  edg0usgr  27822  nbuhgr  27912  nbumgr  27916  nbuhgr2vtx1edgblem  27920  cusgredg  27993  cusgrsize2inds  28022  sizusglecusg  28032  umgr2v2enb1  28095  rusgr1vtx  28157  uspgr2wlkeq  28215  wlkreslem  28238  spthonepeq  28321  usgr2trlspth  28330  clwlkl1loop  28352  lfgrn1cycl  28371  uspgrn2crct  28374  crctcshwlkn0lem3  28378  crctcshwlkn0lem5  28380  wwlksnextbi  28460  wwlksnredwwlkn0  28462  wwlksnextinj  28465  wspthsnonn0vne  28483  umgr2adedgspth  28514  umgr2wlk  28515  usgr2wspthons3  28530  clwlkclwwlklem2a1  28557  clwlkclwwlklem2fv2  28561  clwlkclwwlklem2a4  28562  clwlkclwwlklem2a  28563  clwlkclwwlklem2  28565  clwwisshclwws  28580  erclwwlktr  28587  clwwlkn1loopb  28608  clwwlknwwlksnb  28620  clwwlkext2edg  28621  erclwwlkntr  28636  clwwlknon1  28662  clwwlknonwwlknonb  28671  clwwlknonex2lem2  28673  upgr1wlkdlem1  28710  upgr3v3e3cycl  28745  uhgr3cyclex  28747  upgr4cycl4dv4e  28750  eucrctshift  28808  frgr3vlem1  28838  3cyclfrgrrn1  28850  3cyclfrgrrn  28851  4cycl2vnunb  28855  frgrnbnb  28858  frgrncvvdeqlem8  28871  frgrwopreglem5  28886  frgrwopreglem5ALT  28887  frgr2wwlk1  28894  2clwwlk2clwwlk  28915  numclwwlk1lem2fo  28923  frgrreg  28959  friendshipgt3  28963  shmodsi  29952  kbass6  30684  mdsymlem6  30971  mdsymlem7  30972  cdj3lem2a  30999  cdj3lem3a  31002  satfrel  33541  gonarlem  33568  satffunlem1lem1  33576  satffunlem2lem1  33578  satffun  33583  wl-spae  35778  grpomndo  36131  rngoueqz  36196  zerdivemp1x  36203  elpcliN  38154  dflim5  41303  relexpiidm  41622  relexpxpmin  41635  ntrk0kbimka  41959  eel12131  42643  tratrbVD  42791  2uasbanhVD  42841  funressnfv  44877  funbrafv  44990  otiunsndisjX  45111  ssfz12  45146  fzoopth  45159  iccpartgt  45219  iccelpart  45225  iccpartnel  45230  fargshiftf1  45233  sprsymrelfvlem  45282  sprsymrelf1lem  45283  prproropf1olem4  45298  sbcpr  45313  reupr  45314  poprelb  45316  reuopreuprim  45318  fmtno4prmfac  45364  lighneallem4b  45401  lighneal  45403  mogoldbblem  45512  gbegt5  45553  sbgoldbaltlem1  45571  sbgoldbm  45576  bgoldbtbndlem2  45598  bgoldbtbndlem3  45599  bgoldbtbndlem4  45600  bgoldbtbnd  45601  isomuspgrlem2b  45621  isomuspgrlem2d  45623  lidldomn1  45819  2zrngamgm  45837  rngccatidALTV  45887  ringccatidALTV  45950  nzerooringczr  45970  scmsuppss  46048  ply1mulgsumlem1  46067  lincsumcl  46112  ellcoellss  46116  lindslinindsimp1  46138  lindslinindimp2lem1  46139  nn0sumshdiglemA  46305  nn0sumshdiglemB  46306  itschlc0xyqsol1  46452