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  1641  preqsnd  4835  3elpr2eq  4882  propeqop  5482  po2ne  5577  funopg  6570  eldmrexrnb  7082  fvn0fvelrnOLD  7153  peano5  7889  f1o2ndf1  8121  suppimacnv  8173  omordi  8578  omeulem1  8594  brecop  8824  isinf  9268  isinfOLD  9269  fiint  9338  fiintOLD  9339  carduni  9995  dfac5  10143  dfac2b  10145  cofsmo  10283  cfcoflem  10286  domtriomlem  10456  axdc3lem2  10465  nqereu  10943  squeeze0  12145  zmax  12961  elpq  12991  xnn0lenn0nn0  13261  xrsupsslem  13323  xrinfmsslem  13324  supxrunb1  13335  supxrunb2  13336  difreicc  13501  elfz0ubfz0  13649  elfz0fzfz0  13650  fz0fzelfz0  13651  fz0fzdiffz0  13654  fzo1fzo0n0  13731  elfzodifsumelfzo  13747  ssfzo12  13775  ssfzo12bi  13777  fzoopth  13778  elfznelfzo  13788  injresinjlem  13803  injresinj  13804  addmodlteq  13964  uzindi  14000  ssnn0fi  14003  suppssfz  14012  facwordi  14307  hasheqf1oi  14369  hashf1rn  14370  fundmge2nop0  14520  swrdswrdlem  14722  swrdswrd  14723  wrd2ind  14741  swrdccatin1  14743  pfxccatin12lem2  14749  swrdccat  14753  reuccatpfxs1lem  14764  repsdf2  14796  cshwidx0  14824  cshweqrep  14839  2cshwcshw  14844  cshwcsh2id  14847  swrdco  14856  wwlktovfo  14977  sqrt2irr  16267  oddnn02np1  16367  oddge22np1  16368  evennn02n  16369  evennn2n  16370  dfgcd2  16565  lcmf  16652  lcmfunsnlem2lem2  16658  initoeu2lem1  18027  symgfix2  19397  gsmsymgreqlem2  19412  psgnunilem4  19478  01eq0ringOLD  20491  lmodfopnelem1  20855  nzerooringczr  21441  cply1mul  22234  gsummoncoe1  22246  mamufacex  22334  matecl  22363  gsummatr01  22597  mp2pm2mplem4  22747  chfacfscmul0  22796  chfacfpmmul0  22800  cayhamlem1  22804  fbunfip  23807  tngngp3  24595  mpomulcn  24809  zabsle1  27259  gausslemma2dlem1a  27328  2lgsoddprm  27379  2sqreunnltblem  27414  umgrnloopv  29085  upgredg2vtx  29120  usgruspgrb  29162  usgrnloopvALT  29180  usgredg2vlem2  29205  edg0usgr  29232  nbuhgr  29322  nbumgr  29326  nbuhgr2vtx1edgblem  29330  cusgredg  29403  cusgrsize2inds  29433  sizusglecusg  29443  umgr2v2enb1  29506  rusgr1vtx  29568  uspgr2wlkeq  29626  wlkreslem  29649  spthonepeq  29734  usgr2trlspth  29743  clwlkl1loop  29765  lfgrn1cycl  29787  uspgrn2crct  29790  crctcshwlkn0lem3  29794  crctcshwlkn0lem5  29796  wwlksnextbi  29876  wwlksnredwwlkn0  29878  wwlksnextinj  29881  wspthsnonn0vne  29899  umgr2adedgspth  29930  umgr2wlk  29931  usgr2wspthons3  29946  clwlkclwwlklem2a1  29973  clwlkclwwlklem2fv2  29977  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  clwlkclwwlklem2  29981  clwwisshclwws  29996  erclwwlktr  30003  clwwlkn1loopb  30024  clwwlknwwlksnb  30036  clwwlkext2edg  30037  erclwwlkntr  30052  clwwlknon1  30078  clwwlknonwwlknonb  30087  clwwlknonex2lem2  30089  upgr1wlkdlem1  30126  upgr3v3e3cycl  30161  uhgr3cyclex  30163  upgr4cycl4dv4e  30166  eucrctshift  30224  frgr3vlem1  30254  3cyclfrgrrn1  30266  3cyclfrgrrn  30267  4cycl2vnunb  30271  frgrnbnb  30274  frgrncvvdeqlem8  30287  frgrwopreglem5  30302  frgrwopreglem5ALT  30303  frgr2wwlk1  30310  2clwwlk2clwwlk  30331  numclwwlk1lem2fo  30339  frgrreg  30375  friendshipgt3  30379  shmodsi  31370  kbass6  32102  mdsymlem6  32389  mdsymlem7  32390  cdj3lem2a  32417  cdj3lem3a  32420  satfrel  35389  gonarlem  35416  satffunlem1lem1  35424  satffunlem2lem1  35426  satffun  35431  wl-spae  37539  grpomndo  37899  rngoueqz  37964  zerdivemp1x  37971  elpcliN  39912  dflim5  43353  relexpiidm  43728  relexpxpmin  43741  ntrk0kbimka  44063  eel12131  44737  tratrbVD  44885  2uasbanhVD  44935  funressnfv  47072  funbrafv  47187  otiunsndisjX  47308  ssfz12  47343  iccpartgt  47441  iccelpart  47447  iccpartnel  47452  fargshiftf1  47455  sprsymrelfvlem  47504  sprsymrelf1lem  47505  prproropf1olem4  47520  sbcpr  47535  reupr  47536  poprelb  47538  reuopreuprim  47540  fmtno4prmfac  47586  lighneallem4b  47623  lighneal  47625  mogoldbblem  47734  gbegt5  47775  sbgoldbaltlem1  47793  sbgoldbm  47798  bgoldbtbndlem2  47820  bgoldbtbndlem3  47821  bgoldbtbndlem4  47822  bgoldbtbnd  47823  grimedg  47948  cycl3grtri  47959  grlimgrtri  48008  lidldomn1  48206  2zrngamgm  48220  rngccatidALTV  48247  ringccatidALTV  48281  scmsuppss  48346  ply1mulgsumlem1  48362  lincsumcl  48407  ellcoellss  48411  lindslinindsimp1  48433  lindslinindimp2lem1  48434  nn0sumshdiglemA  48599  nn0sumshdiglemB  48600  itschlc0xyqsol1  48746