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  1642  preqsnd  4811  3elpr2eq  4858  propeqop  5447  po2ne  5540  funopg  6515  eldmrexrnb  7025  peano5  7823  f1o2ndf1  8052  suppimacnv  8104  omordi  8481  omeulem1  8497  brecop  8734  isinf  9149  fiint  9211  carduni  9874  dfac5  10020  dfac2b  10022  cofsmo  10160  cfcoflem  10163  domtriomlem  10333  axdc3lem2  10342  nqereu  10820  squeeze0  12025  zmax  12843  elpq  12873  xnn0lenn0nn0  13144  xrsupsslem  13206  xrinfmsslem  13207  supxrunb1  13218  supxrunb2  13219  difreicc  13384  elfz0ubfz0  13532  elfz0fzfz0  13533  fz0fzelfz0  13534  fz0fzdiffz0  13537  fzo1fzo0n0  13615  elfzodifsumelfzo  13631  ssfzo12  13659  ssfzo12bi  13661  fzoopth  13662  elfznelfzo  13673  injresinjlem  13690  injresinj  13691  addmodlteq  13853  uzindi  13889  ssnn0fi  13892  suppssfz  13901  facwordi  14196  hasheqf1oi  14258  hashf1rn  14259  fundmge2nop0  14409  swrdswrdlem  14611  swrdswrd  14612  wrd2ind  14630  swrdccatin1  14632  pfxccatin12lem2  14638  swrdccat  14642  reuccatpfxs1lem  14653  repsdf2  14685  cshwidx0  14713  cshweqrep  14728  2cshwcshw  14732  cshwcsh2id  14735  swrdco  14744  wwlktovfo  14865  sqrt2irr  16158  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  dfgcd2  16457  lcmf  16544  lcmfunsnlem2lem2  16550  initoeu2lem1  17921  symgfix2  19329  gsmsymgreqlem2  19344  psgnunilem4  19410  01eq0ringOLD  20447  lmodfopnelem1  20832  nzerooringczr  21418  cply1mul  22212  gsummoncoe1  22224  mamufacex  22312  matecl  22341  gsummatr01  22575  mp2pm2mplem4  22725  chfacfscmul0  22774  chfacfpmmul0  22778  cayhamlem1  22782  fbunfip  23785  tngngp3  24572  mpomulcn  24786  zabsle1  27235  gausslemma2dlem1a  27304  2lgsoddprm  27355  2sqreunnltblem  27390  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  29625  wlkreslem  29647  spthonepeq  29731  usgr2trlspth  29740  clwlkl1loop  29762  lfgrn1cycl  29784  uspgrn2crct  29787  crctcshwlkn0lem3  29791  crctcshwlkn0lem5  29793  wwlksnextbi  29873  wwlksnredwwlkn0  29875  wwlksnextinj  29878  wspthsnonn0vne  29896  umgr2adedgspth  29927  umgr2wlk  29928  usgr2wspthons3  29943  clwlkclwwlklem2a1  29970  clwlkclwwlklem2fv2  29974  clwlkclwwlklem2a4  29975  clwlkclwwlklem2a  29976  clwlkclwwlklem2  29978  clwwisshclwws  29993  erclwwlktr  30000  clwwlkn1loopb  30021  clwwlknwwlksnb  30033  clwwlkext2edg  30034  erclwwlkntr  30049  clwwlknon1  30075  clwwlknonwwlknonb  30084  clwwlknonex2lem2  30086  upgr1wlkdlem1  30123  upgr3v3e3cycl  30158  uhgr3cyclex  30160  upgr4cycl4dv4e  30163  eucrctshift  30221  frgr3vlem1  30251  3cyclfrgrrn1  30263  3cyclfrgrrn  30264  4cycl2vnunb  30268  frgrnbnb  30271  frgrncvvdeqlem8  30284  frgrwopreglem5  30299  frgrwopreglem5ALT  30300  frgr2wwlk1  30307  2clwwlk2clwwlk  30328  numclwwlk1lem2fo  30336  frgrreg  30372  friendshipgt3  30376  shmodsi  31367  kbass6  32099  mdsymlem6  32386  mdsymlem7  32387  cdj3lem2a  32414  cdj3lem3a  32417  satfrel  35409  gonarlem  35436  satffunlem1lem1  35444  satffunlem2lem1  35446  satffun  35451  wl-spae  37561  grpomndo  37921  rngoueqz  37986  zerdivemp1x  37993  elpcliN  39938  dflim5  43368  relexpiidm  43743  relexpxpmin  43756  ntrk0kbimka  44078  eel12131  44751  tratrbVD  44899  2uasbanhVD  44949  funressnfv  47080  funbrafv  47195  otiunsndisjX  47316  ssfz12  47351  iccpartgt  47464  iccelpart  47470  iccpartnel  47475  fargshiftf1  47478  sprsymrelfvlem  47527  sprsymrelf1lem  47528  prproropf1olem4  47543  sbcpr  47558  reupr  47559  poprelb  47561  reuopreuprim  47563  fmtno4prmfac  47609  lighneallem4b  47646  lighneal  47648  mogoldbblem  47757  gbegt5  47798  sbgoldbaltlem1  47816  sbgoldbm  47821  bgoldbtbndlem2  47843  bgoldbtbndlem3  47844  bgoldbtbndlem4  47845  bgoldbtbnd  47846  grimedg  47972  cycl3grtri  47984  grlimgrtri  48040  pgnbgreunbgrlem2lem1  48151  pgnbgreunbgrlem2lem2  48152  pgnbgreunbgrlem2lem3  48153  lidldomn1  48268  2zrngamgm  48282  rngccatidALTV  48309  ringccatidALTV  48343  scmsuppss  48408  ply1mulgsumlem1  48424  lincsumcl  48469  ellcoellss  48473  lindslinindsimp1  48495  lindslinindimp2lem1  48496  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658  itschlc0xyqsol1  48804