Theorem com13 89

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 88	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com23 87	1 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com24  96  an13s  664  an31s  667  3imp31  1129  3imp21  1131  meredith  1673  preqsnd  4813  3elpr2eq  4833  propeqop  5478  po2ne  5574  funopg  6574  eldmrexrnb  7092  peano5  7905  f1o2ndf1  8135  suppimacnv  8194  omordi  8577  omeulem1  8593  brecop  8834  isinf  9259  fiint  9321  carduni  10065  dfac5  10210  dfac2b  10212  cofsmo  10350  cfcoflem  10353  domtriomlem  10523  axdc3lem2  10532  nqereu  11017  squeeze0  12223  zmax  13075  elpq  13106  xnn0lenn0nn0  13378  xrsupsslem  13440  xrinfmsslem  13441  supxrunb1  13452  supxrunb2  13453  difreicc  13618  elfz0ubfz0  13769  elfz0fzfz0  13770  fz0fzelfz0  13771  fz0fzdiffz0  13774  fzo1fzo0n0  13853  elfzodifsumelfzo  13869  ssfzo12  13897  ssfzo12bi  13899  fzoopth  13900  elfznelfzo  13911  injresinjlem  13928  injresinj  13929  addmodlteq  14092  uzindi  14128  ssnn0fi  14131  suppssfz  14140  facwordi  14436  hasheqf1oi  14498  hashf1rn  14499  fundmge2nop0  14650  swrdswrdlem  14857  swrdswrd  14858  wrd2ind  14876  swrdccatin1  14878  pfxccatin12lem2  14884  swrdccat  14888  reuccatpfxs1lem  14899  repsdf2  14933  cshwidx0  14961  cshweqrep  14976  2cshwcshw  14980  cshwcsh2id  14983  swrdco  14992  wwlktovfo  15116  sqrt2irr  16422  oddnn02np1  16523  oddge22np1  16524  evennn02n  16525  evennn2n  16526  dfgcd2  16724  lcmf  16813  lcmfunsnlem2lem2  16819  initoeu2lem1  18194  symgfix2  19635  gsmsymgreqlem2  19650  psgnunilem4  19716  01eq0ringOLD  20787  lmodfopnelem1  21178  nzerooringczr  21791  cply1mul  22619  gsummoncoe1  22631  mamufacex  22716  matecl  22745  gsummatr01  22979  mp2pm2mplem4  23132  chfacfscmul0  23181  chfacfpmmul0  23185  cayhamlem1  23189  fbunfip  24193  tngngp3  24980  mpomulcn  25193  zabsle1  27628  gausslemma2dlem1a  27697  2lgsoddprm  27748  2sqreunnltblem  27783  fltoprmlem2  27999  umgrnloopv  29689  upgredg2vtx  29724  usgruspgrb  29769  usgrnloopvALT  29787  usgredg2vlem2  29812  edg0usgr  29839  nbuhgr  29929  nbumgr  29933  nbuhgr2vtx1edgblem  29937  cusgredg  30010  cusgrsize2inds  30039  sizusglecusg  30049  umgr2v2enb1  30112  rusgr1vtx  30174  uspgr2wlkeq  30231  wlkreslem  30253  spthonepeq  30343  usgr2trlspth  30352  clwlkl1loop  30375  lfgrn1cycl  30399  uspgrn2crct  30402  crctcshwlkn0lem3  30406  crctcshwlkn0lem5  30408  wwlksnextbi  30488  wwlksnredwwlkn0  30490  wwlksnextinj  30493  wspthsnonn0vne  30511  umgr2adedgspth  30542  umgr2wlk  30543  usgr2wspthons3  30561  clwlkclwwlklem2a1  30588  clwlkclwwlklem2fv2  30592  clwlkclwwlklem2a4  30593  clwlkclwwlklem2a  30594  clwlkclwwlklem2  30596  clwwisshclwws  30611  erclwwlktr  30618  clwwlkn1loopb  30639  clwwlknwwlksnb  30651  clwwlkext2edg  30652  erclwwlkntr  30667  clwwlknon1  30693  clwwlknonwwlknonb  30702  clwwlknonex2lem2  30704  upgr1wlkdlem1  30741  upgr3v3e3cycl  30786  uhgr3cyclex  30788  upgr4cycl4dv4e  30791  eucrctshift  30849  frgr3vlem1  30879  3cyclfrgrrn1  30891  3cyclfrgrrn  30892  4cycl2vnunb  30896  frgrnbnb  30899  frgrncvvdeqlem8  30912  frgrwopreglem5  30927  frgrwopreglem5ALT  30928  frgr2wwlk1  30935  2clwwlk2clwwlk  30956  numclwwlk1lem2fo  30964  frgrreg  31000  friendshipgt3  31004  shmodsi  31996  kbass6  32728  mdsymlem6  33015  mdsymlem7  33016  cdj3lem2a  33043  cdj3lem3a  33046  satfrel  36218  gonarlem  36245  satffunlem1lem1  36253  satffunlem2lem1  36255  satffun  36260  wl-spae  38546  grpomndo  38902  rngoueqz  38967  zerdivemp1x  38974  elpcliN  41043  dflim5  44424  relexpiidm  44797  relexpxpmin  44810  ntrk0kbimka  45132  eel12131  45788  tratrbVD  45936  2uasbanhVD  45986  funressnfv  48206  funbrafv  48321  otiunsndisjX  48442  ssfz12  48477  iccpartgt  48602  iccelpart  48608  iccpartnel  48613  fargshiftf1  48616  sprsymrelfvlem  48665  sprsymrelf1lem  48666  prproropf1olem4  48681  sbcpr  48696  reupr  48697  poprelb  48699  reuopreuprim  48701  fmtno4prmfac  48750  lighneallem4b  48787  lighneal  48789  nprmdvdsfacm1lem2  48799  mogoldbblem  48911  gbegt5  48952  sbgoldbaltlem1  48970  sbgoldbm  48975  bgoldbtbndlem2  48997  bgoldbtbndlem3  48998  bgoldbtbndlem4  48999  bgoldbtbnd  49000  grimedg  49126  cycl3grtri  49138  grlimgrtri  49194  pgnbgreunbgrlem2lem1  49305  pgnbgreunbgrlem2lem2  49306  pgnbgreunbgrlem2lem3  49307  lidldomn1  49421  2zrngamgm  49435  rngccatidALTV  49462  ringccatidALTV  49496  scmsuppss  49576  ply1mulgsumlem1  49591  lincsumcl  49636  ellcoellss  49640  lindslinindsimp1  49662  lindslinindimp2lem1  49663  nn0sumshdiglemA  49824  nn0sumshdiglemB  49825  itschlc0xyqsol1  49971