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 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

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  96  an13s  663  an31s  666  3imp31  1127  3imp21  1129  meredith  1668  preqsnd  4825  3elpr2eq  4872  propeqop  5488  po2ne  5583  funopg  6567  eldmrexrnb  7085  peano5  7886  f1o2ndf1  8113  suppimacnv  8166  omordi  8547  omeulem1  8563  brecop  8804  isinf  9221  fiint  9282  carduni  9963  dfac5  10108  dfac2b  10110  cofsmo  10249  cfcoflem  10252  domtriomlem  10422  axdc3lem2  10431  nqereu  10910  squeeze0  12114  zmax  12965  elpq  12995  xnn0lenn0nn0  13267  xrsupsslem  13329  xrinfmsslem  13330  supxrunb1  13341  supxrunb2  13342  difreicc  13507  elfz0ubfz0  13656  elfz0fzfz0  13657  fz0fzelfz0  13658  fz0fzdiffz0  13661  fzo1fzo0n0  13740  elfzodifsumelfzo  13756  ssfzo12  13784  ssfzo12bi  13786  fzoopth  13787  elfznelfzo  13798  injresinjlem  13815  injresinj  13816  addmodlteq  13978  uzindi  14014  ssnn0fi  14017  suppssfz  14026  facwordi  14321  hasheqf1oi  14383  hashf1rn  14384  fundmge2nop0  14535  swrdswrdlem  14737  swrdswrd  14738  wrd2ind  14756  swrdccatin1  14758  pfxccatin12lem2  14764  swrdccat  14768  reuccatpfxs1lem  14779  repsdf2  14811  cshwidx0  14839  cshweqrep  14854  2cshwcshw  14858  cshwcsh2id  14861  swrdco  14870  wwlktovfo  14991  sqrt2irr  16301  oddnn02np1  16402  oddge22np1  16403  evennn02n  16404  evennn2n  16405  dfgcd2  16600  lcmf  16687  lcmfunsnlem2lem2  16693  initoeu2lem1  18067  symgfix2  19482  gsmsymgreqlem2  19497  psgnunilem4  19563  01eq0ringOLD  20611  lmodfopnelem1  20993  nzerooringczr  21595  cply1mul  22421  gsummoncoe1  22433  mamufacex  22518  matecl  22547  gsummatr01  22781  mp2pm2mplem4  22931  chfacfscmul0  22980  chfacfpmmul0  22984  cayhamlem1  22988  fbunfip  23991  tngngp3  24778  mpomulcn  24991  zabsle1  27422  gausslemma2dlem1a  27491  2lgsoddprm  27542  2sqreunnltblem  27577  umgrnloopv  29393  upgredg2vtx  29428  usgruspgrb  29470  usgrnloopvALT  29488  usgredg2vlem2  29513  edg0usgr  29540  nbuhgr  29630  nbumgr  29634  nbuhgr2vtx1edgblem  29638  cusgredg  29711  cusgrsize2inds  29740  sizusglecusg  29750  umgr2v2enb1  29813  rusgr1vtx  29875  uspgr2wlkeq  29932  wlkreslem  29954  spthonepeq  30038  usgr2trlspth  30047  clwlkl1loop  30069  lfgrn1cycl  30091  uspgrn2crct  30094  crctcshwlkn0lem3  30098  crctcshwlkn0lem5  30100  wwlksnextbi  30180  wwlksnredwwlkn0  30182  wwlksnextinj  30185  wspthsnonn0vne  30203  umgr2adedgspth  30234  umgr2wlk  30235  usgr2wspthons3  30253  clwlkclwwlklem2a1  30280  clwlkclwwlklem2fv2  30284  clwlkclwwlklem2a4  30285  clwlkclwwlklem2a  30286  clwlkclwwlklem2  30288  clwwisshclwws  30303  erclwwlktr  30310  clwwlkn1loopb  30331  clwwlknwwlksnb  30343  clwwlkext2edg  30344  erclwwlkntr  30359  clwwlknon1  30385  clwwlknonwwlknonb  30394  clwwlknonex2lem2  30396  upgr1wlkdlem1  30433  upgr3v3e3cycl  30468  uhgr3cyclex  30470  upgr4cycl4dv4e  30473  eucrctshift  30531  frgr3vlem1  30561  3cyclfrgrrn1  30573  3cyclfrgrrn  30574  4cycl2vnunb  30578  frgrnbnb  30581  frgrncvvdeqlem8  30594  frgrwopreglem5  30609  frgrwopreglem5ALT  30610  frgr2wwlk1  30617  2clwwlk2clwwlk  30638  numclwwlk1lem2fo  30646  frgrreg  30682  friendshipgt3  30686  shmodsi  31678  kbass6  32410  mdsymlem6  32697  mdsymlem7  32698  cdj3lem2a  32725  cdj3lem3a  32728  satfrel  35754  gonarlem  35781  satffunlem1lem1  35789  satffunlem2lem1  35791  satffun  35796  wl-spae  38059  grpomndo  38409  rngoueqz  38474  zerdivemp1x  38481  elpcliN  40552  dflim5  43941  relexpiidm  44315  relexpxpmin  44328  ntrk0kbimka  44650  eel12131  45306  tratrbVD  45454  2uasbanhVD  45504  funressnfv  47662  funbrafv  47777  otiunsndisjX  47898  ssfz12  47933  iccpartgt  48058  iccelpart  48064  iccpartnel  48069  fargshiftf1  48072  sprsymrelfvlem  48121  sprsymrelf1lem  48122  prproropf1olem4  48137  sbcpr  48152  reupr  48153  poprelb  48155  reuopreuprim  48157  fmtno4prmfac  48206  lighneallem4b  48243  lighneal  48245  nprmdvdsfacm1lem2  48255  mogoldbblem  48367  gbegt5  48408  sbgoldbaltlem1  48426  sbgoldbm  48431  bgoldbtbndlem2  48453  bgoldbtbndlem3  48454  bgoldbtbndlem4  48455  bgoldbtbnd  48456  grimedg  48582  cycl3grtri  48594  grlimgrtri  48650  pgnbgreunbgrlem2lem1  48761  pgnbgreunbgrlem2lem2  48762  pgnbgreunbgrlem2lem3  48763  lidldomn1  48878  2zrngamgm  48892  rngccatidALTV  48919  ringccatidALTV  48953  scmsuppss  49029  ply1mulgsumlem1  49044  lincsumcl  49089  ellcoellss  49093  lindslinindsimp1  49115  lindslinindimp2lem1  49116  nn0sumshdiglemA  49277  nn0sumshdiglemB  49278  itschlc0xyqsol1  49424