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  1637  preqsnd  4863  3elpr2eq  4910  propeqop  5516  po2ne  5612  funopg  6601  eldmrexrnb  7111  fvn0fvelrnOLD  7182  peano5  7915  f1o2ndf1  8145  suppimacnv  8197  omordi  8602  omeulem1  8618  brecop  8848  isinf  9293  isinfOLD  9294  fiint  9363  fiintOLD  9364  carduni  10018  dfac5  10166  dfac2b  10168  cofsmo  10306  cfcoflem  10309  domtriomlem  10479  axdc3lem2  10488  nqereu  10966  squeeze0  12168  zmax  12984  elpq  13014  xnn0lenn0nn0  13283  xrsupsslem  13345  xrinfmsslem  13346  supxrunb1  13357  supxrunb2  13358  difreicc  13520  elfz0ubfz0  13668  elfz0fzfz0  13669  fz0fzelfz0  13670  fz0fzdiffz0  13673  fzo1fzo0n0  13750  elfzodifsumelfzo  13766  ssfzo12  13794  ssfzo12bi  13796  fzoopth  13797  elfznelfzo  13807  injresinjlem  13822  injresinj  13823  addmodlteq  13983  uzindi  14019  ssnn0fi  14022  suppssfz  14031  facwordi  14324  hasheqf1oi  14386  hashf1rn  14387  fundmge2nop0  14537  swrdswrdlem  14738  swrdswrd  14739  wrd2ind  14757  swrdccatin1  14759  pfxccatin12lem2  14765  swrdccat  14769  reuccatpfxs1lem  14780  repsdf2  14812  cshwidx0  14840  cshweqrep  14855  2cshwcshw  14860  cshwcsh2id  14863  swrdco  14872  wwlktovfo  14993  sqrt2irr  16281  oddnn02np1  16381  oddge22np1  16382  evennn02n  16383  evennn2n  16384  dfgcd2  16579  lcmf  16666  lcmfunsnlem2lem2  16672  initoeu2lem1  18067  symgfix2  19448  gsmsymgreqlem2  19463  psgnunilem4  19529  01eq0ringOLD  20547  lmodfopnelem1  20912  nzerooringczr  21508  cply1mul  22315  gsummoncoe1  22327  mamufacex  22415  matecl  22446  gsummatr01  22680  mp2pm2mplem4  22830  chfacfscmul0  22879  chfacfpmmul0  22883  cayhamlem1  22887  fbunfip  23892  tngngp3  24692  mpomulcn  24904  zabsle1  27354  gausslemma2dlem1a  27423  2lgsoddprm  27474  2sqreunnltblem  27509  umgrnloopv  29137  upgredg2vtx  29172  usgruspgrb  29214  usgrnloopvALT  29232  usgredg2vlem2  29257  edg0usgr  29284  nbuhgr  29374  nbumgr  29378  nbuhgr2vtx1edgblem  29382  cusgredg  29455  cusgrsize2inds  29485  sizusglecusg  29495  umgr2v2enb1  29558  rusgr1vtx  29620  uspgr2wlkeq  29678  wlkreslem  29701  spthonepeq  29784  usgr2trlspth  29793  clwlkl1loop  29815  lfgrn1cycl  29834  uspgrn2crct  29837  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  wwlksnextbi  29923  wwlksnredwwlkn0  29925  wwlksnextinj  29928  wspthsnonn0vne  29946  umgr2adedgspth  29977  umgr2wlk  29978  usgr2wspthons3  29993  clwlkclwwlklem2a1  30020  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwwisshclwws  30043  erclwwlktr  30050  clwwlkn1loopb  30071  clwwlknwwlksnb  30083  clwwlkext2edg  30084  erclwwlkntr  30099  clwwlknon1  30125  clwwlknonwwlknonb  30134  clwwlknonex2lem2  30136  upgr1wlkdlem1  30173  upgr3v3e3cycl  30208  uhgr3cyclex  30210  upgr4cycl4dv4e  30213  eucrctshift  30271  frgr3vlem1  30301  3cyclfrgrrn1  30313  3cyclfrgrrn  30314  4cycl2vnunb  30318  frgrnbnb  30321  frgrncvvdeqlem8  30334  frgrwopreglem5  30349  frgrwopreglem5ALT  30350  frgr2wwlk1  30357  2clwwlk2clwwlk  30378  numclwwlk1lem2fo  30386  frgrreg  30422  friendshipgt3  30426  shmodsi  31417  kbass6  32149  mdsymlem6  32436  mdsymlem7  32437  cdj3lem2a  32464  cdj3lem3a  32467  satfrel  35351  gonarlem  35378  satffunlem1lem1  35386  satffunlem2lem1  35388  satffun  35393  wl-spae  37501  grpomndo  37861  rngoueqz  37926  zerdivemp1x  37933  elpcliN  39875  dflim5  43318  relexpiidm  43693  relexpxpmin  43706  ntrk0kbimka  44028  eel12131  44710  tratrbVD  44858  2uasbanhVD  44908  funressnfv  46992  funbrafv  47107  otiunsndisjX  47228  ssfz12  47263  iccpartgt  47351  iccelpart  47357  iccpartnel  47362  fargshiftf1  47365  sprsymrelfvlem  47414  sprsymrelf1lem  47415  prproropf1olem4  47430  sbcpr  47445  reupr  47446  poprelb  47448  reuopreuprim  47450  fmtno4prmfac  47496  lighneallem4b  47533  lighneal  47535  mogoldbblem  47644  gbegt5  47685  sbgoldbaltlem1  47703  sbgoldbm  47708  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  grimedg  47840  grlimgrtri  47898  lidldomn1  48074  2zrngamgm  48088  rngccatidALTV  48115  ringccatidALTV  48149  scmsuppss  48215  ply1mulgsumlem1  48231  lincsumcl  48276  ellcoellss  48280  lindslinindsimp1  48302  lindslinindimp2lem1  48303  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  itschlc0xyqsol1  48615