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  1674  preqsnd  4817  3elpr2eq  4837  propeqop  5483  po2ne  5579  funopg  6594  eldmrexrnb  7116  peano5  7929  f1o2ndf1  8160  suppimacnv  8219  omordi  8602  omeulem1  8618  brecop  8859  isinf  9284  fiint  9346  carduni  10089  dfac5  10234  dfac2b  10236  cofsmo  10374  cfcoflem  10377  domtriomlem  10547  axdc3lem2  10556  nqereu  11041  squeeze0  12247  zmax  13099  elpq  13130  xnn0lenn0nn0  13402  xrsupsslem  13464  xrinfmsslem  13465  supxrunb1  13476  supxrunb2  13477  difreicc  13642  elfz0ubfz0  13793  elfz0fzfz0  13794  fz0fzelfz0  13795  fz0fzdiffz0  13798  fzo1fzo0n0  13877  elfzodifsumelfzo  13893  ssfzo12  13921  ssfzo12bi  13923  fzoopth  13924  elfznelfzo  13935  injresinjlem  13952  injresinj  13953  addmodlteq  14116  uzindi  14152  ssnn0fi  14155  suppssfz  14164  facwordi  14460  hasheqf1oi  14522  hashf1rn  14523  fundmge2nop0  14674  swrdswrdlem  14881  swrdswrd  14882  wrd2ind  14900  swrdccatin1  14902  pfxccatin12lem2  14908  swrdccat  14912  reuccatpfxs1lem  14923  repsdf2  14957  cshwidx0  14985  cshweqrep  15000  2cshwcshw  15004  cshwcsh2id  15007  swrdco  15016  wwlktovfo  15140  sqrt2irr  16446  oddnn02np1  16547  oddge22np1  16548  evennn02n  16549  evennn2n  16550  dfgcd2  16748  lcmf  16837  lcmfunsnlem2lem2  16843  initoeu2lem1  18218  symgfix2  19660  gsmsymgreqlem2  19675  psgnunilem4  19741  01eq0ringOLD  20812  lmodfopnelem1  21203  nzerooringczr  21816  cply1mul  22644  gsummoncoe1  22656  mamufacex  22741  matecl  22770  gsummatr01  23004  mp2pm2mplem4  23157  chfacfscmul0  23206  chfacfpmmul0  23210  cayhamlem1  23214  fbunfip  24218  tngngp3  25005  mpomulcn  25218  zabsle1  27653  gausslemma2dlem1a  27722  2lgsoddprm  27773  2sqreunnltblem  27808  fltoprmlem2  28024  umgrnloopv  29714  upgredg2vtx  29749  usgruspgrb  29794  usgrnloopvALT  29812  usgredg2vlem2  29837  edg0usgr  29864  nbuhgr  29954  nbumgr  29958  nbuhgr2vtx1edgblem  29962  cusgredg  30035  cusgrsize2inds  30064  sizusglecusg  30074  umgr2v2enb1  30137  rusgr1vtx  30199  uspgr2wlkeq  30256  wlkreslem  30278  spthonepeq  30368  usgr2trlspth  30377  clwlkl1loop  30400  lfgrn1cycl  30424  uspgrn2crct  30427  crctcshwlkn0lem3  30431  crctcshwlkn0lem5  30433  wwlksnextbi  30513  wwlksnredwwlkn0  30515  wwlksnextinj  30518  wspthsnonn0vne  30536  umgr2adedgspth  30567  umgr2wlk  30568  usgr2wspthons3  30586  clwlkclwwlklem2a1  30613  clwlkclwwlklem2fv2  30617  clwlkclwwlklem2a4  30618  clwlkclwwlklem2a  30619  clwlkclwwlklem2  30621  clwwisshclwws  30636  erclwwlktr  30643  clwwlkn1loopb  30664  clwwlknwwlksnb  30676  clwwlkext2edg  30677  erclwwlkntr  30692  clwwlknon1  30718  clwwlknonwwlknonb  30727  clwwlknonex2lem2  30729  upgr1wlkdlem1  30766  upgr3v3e3cycl  30811  uhgr3cyclex  30813  upgr4cycl4dv4e  30816  eucrctshift  30874  frgr3vlem1  30904  3cyclfrgrrn1  30916  3cyclfrgrrn  30917  4cycl2vnunb  30921  frgrnbnb  30924  frgrncvvdeqlem8  30937  frgrwopreglem5  30952  frgrwopreglem5ALT  30953  frgr2wwlk1  30960  2clwwlk2clwwlk  30981  numclwwlk1lem2fo  30989  frgrreg  31025  friendshipgt3  31029  shmodsi  32021  kbass6  32753  mdsymlem6  33040  mdsymlem7  33041  cdj3lem2a  33068  cdj3lem3a  33071  satfrel  36299  gonarlem  36326  satffunlem1lem1  36334  satffunlem2lem1  36336  satffun  36341  wl-spae  38645  grpomndo  39001  rngoueqz  39066  zerdivemp1x  39073  elpcliN  41142  dflim5  44523  relexpiidm  44896  relexpxpmin  44909  ntrk0kbimka  45231  eel12131  45886  tratrbVD  46034  2uasbanhVD  46084  funressnfv  48318  funbrafv  48433  otiunsndisjX  48554  ssfz12  48589  iccpartgt  48714  iccelpart  48720  iccpartnel  48725  fargshiftf1  48728  sprsymrelfvlem  48777  sprsymrelf1lem  48778  prproropf1olem4  48793  sbcpr  48808  reupr  48809  poprelb  48811  reuopreuprim  48813  fmtno4prmfac  48862  lighneallem4b  48899  lighneal  48901  nprmdvdsfacm1lem2  48911  mogoldbblem  49023  gbegt5  49064  sbgoldbaltlem1  49082  sbgoldbm  49087  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  bgoldbtbndlem4  49111  bgoldbtbnd  49112  grimedg  49238  cycl3grtri  49250  grlimgrtri  49306  pgnbgreunbgrlem2lem1  49417  pgnbgreunbgrlem2lem2  49418  pgnbgreunbgrlem2lem3  49419  lidldomn1  49533  2zrngamgm  49547  rngccatidALTV  49574  ringccatidALTV  49608  scmsuppss  49688  ply1mulgsumlem1  49703  lincsumcl  49748  ellcoellss  49752  lindslinindsimp1  49774  lindslinindimp2lem1  49775  nn0sumshdiglemA  49936  nn0sumshdiglemB  49937  itschlc0xyqsol1  50083