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  650  an31s  653  3imp31  1113  3imp21  1115  meredith  1644  preqsnd  4860  3elpr2eq  4908  propeqop  5508  po2ne  5605  funopg  6583  eldmrexrnb  7094  fvn0fvelrnOLD  7161  peano5  7884  peano5OLD  7885  f1o2ndf1  8108  suppimacnv  8159  omordi  8566  omeulem1  8582  brecop  8804  isinf  9260  isinfOLD  9261  fiint  9324  carduni  9976  dfac5  10123  dfac2b  10125  cofsmo  10264  cfcoflem  10267  domtriomlem  10437  axdc3lem2  10446  nqereu  10924  squeeze0  12117  zmax  12929  elpq  12959  xnn0lenn0nn0  13224  xrsupsslem  13286  xrinfmsslem  13287  supxrunb1  13298  supxrunb2  13299  difreicc  13461  elfz0ubfz0  13605  elfz0fzfz0  13606  fz0fzelfz0  13607  fz0fzdiffz0  13610  fzo1fzo0n0  13683  elfzodifsumelfzo  13698  ssfzo12  13725  ssfzo12bi  13727  elfznelfzo  13737  injresinjlem  13752  injresinj  13753  addmodlteq  13911  uzindi  13947  ssnn0fi  13950  suppssfz  13959  facwordi  14249  hasheqf1oi  14311  hashf1rn  14312  fundmge2nop0  14453  swrdswrdlem  14654  swrdswrd  14655  wrd2ind  14673  swrdccatin1  14675  pfxccatin12lem2  14681  swrdccat  14685  reuccatpfxs1lem  14696  repsdf2  14728  cshwidx0  14756  cshweqrep  14771  2cshwcshw  14776  cshwcsh2id  14779  swrdco  14788  wwlktovfo  14909  sqrt2irr  16192  oddnn02np1  16291  oddge22np1  16292  evennn02n  16293  evennn2n  16294  dfgcd2  16488  lcmf  16570  lcmfunsnlem2lem2  16576  initoeu2lem1  17964  symgfix2  19284  gsmsymgreqlem2  19299  psgnunilem4  19365  01eq0ringOLD  20306  lmodfopnelem1  20508  cply1mul  21818  gsummoncoe1  21828  mamufacex  21891  matecl  21927  gsummatr01  22161  mp2pm2mplem4  22311  chfacfscmul0  22360  chfacfpmmul0  22364  cayhamlem1  22368  fbunfip  23373  tngngp3  24173  zabsle1  26799  gausslemma2dlem1a  26868  2lgsoddprm  26919  2sqreunnltblem  26954  umgrnloopv  28366  upgredg2vtx  28401  usgruspgrb  28441  usgrnloopvALT  28458  usgredg2vlem2  28483  edg0usgr  28510  nbuhgr  28600  nbumgr  28604  nbuhgr2vtx1edgblem  28608  cusgredg  28681  cusgrsize2inds  28710  sizusglecusg  28720  umgr2v2enb1  28783  rusgr1vtx  28845  uspgr2wlkeq  28903  wlkreslem  28926  spthonepeq  29009  usgr2trlspth  29018  clwlkl1loop  29040  lfgrn1cycl  29059  uspgrn2crct  29062  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  wwlksnextbi  29148  wwlksnredwwlkn0  29150  wwlksnextinj  29153  wspthsnonn0vne  29171  umgr2adedgspth  29202  umgr2wlk  29203  usgr2wspthons3  29218  clwlkclwwlklem2a1  29245  clwlkclwwlklem2fv2  29249  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwwisshclwws  29268  erclwwlktr  29275  clwwlkn1loopb  29296  clwwlknwwlksnb  29308  clwwlkext2edg  29309  erclwwlkntr  29324  clwwlknon1  29350  clwwlknonwwlknonb  29359  clwwlknonex2lem2  29361  upgr1wlkdlem1  29398  upgr3v3e3cycl  29433  uhgr3cyclex  29435  upgr4cycl4dv4e  29438  eucrctshift  29496  frgr3vlem1  29526  3cyclfrgrrn1  29538  3cyclfrgrrn  29539  4cycl2vnunb  29543  frgrnbnb  29546  frgrncvvdeqlem8  29559  frgrwopreglem5  29574  frgrwopreglem5ALT  29575  frgr2wwlk1  29582  2clwwlk2clwwlk  29603  numclwwlk1lem2fo  29611  frgrreg  29647  friendshipgt3  29651  shmodsi  30642  kbass6  31374  mdsymlem6  31661  mdsymlem7  31662  cdj3lem2a  31689  cdj3lem3a  31692  satfrel  34358  gonarlem  34385  satffunlem1lem1  34393  satffunlem2lem1  34395  satffun  34400  mpomulcn  35162  wl-spae  36390  grpomndo  36743  rngoueqz  36808  zerdivemp1x  36815  elpcliN  38764  dflim5  42079  relexpiidm  42455  relexpxpmin  42468  ntrk0kbimka  42790  eel12131  43474  tratrbVD  43622  2uasbanhVD  43672  funressnfv  45753  funbrafv  45866  otiunsndisjX  45987  ssfz12  46022  fzoopth  46035  iccpartgt  46095  iccelpart  46101  iccpartnel  46106  fargshiftf1  46109  sprsymrelfvlem  46158  sprsymrelf1lem  46159  prproropf1olem4  46174  sbcpr  46189  reupr  46190  poprelb  46192  reuopreuprim  46194  fmtno4prmfac  46240  lighneallem4b  46277  lighneal  46279  mogoldbblem  46388  gbegt5  46429  sbgoldbaltlem1  46447  sbgoldbm  46452  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  bgoldbtbnd  46477  isomuspgrlem2b  46497  isomuspgrlem2d  46499  lidldomn1  46823  2zrngamgm  46837  rngccatidALTV  46887  ringccatidALTV  46950  nzerooringczr  46970  scmsuppss  47048  ply1mulgsumlem1  47067  lincsumcl  47112  ellcoellss  47116  lindslinindsimp1  47138  lindslinindimp2lem1  47139  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  itschlc0xyqsol1  47452