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  1641  preqsnd  4826  3elpr2eq  4873  propeqop  5470  po2ne  5565  funopg  6553  eldmrexrnb  7067  fvn0fvelrnOLD  7138  peano5  7872  f1o2ndf1  8104  suppimacnv  8156  omordi  8533  omeulem1  8549  brecop  8786  isinf  9214  isinfOLD  9215  fiint  9284  fiintOLD  9285  carduni  9941  dfac5  10089  dfac2b  10091  cofsmo  10229  cfcoflem  10232  domtriomlem  10402  axdc3lem2  10411  nqereu  10889  squeeze0  12093  zmax  12911  elpq  12941  xnn0lenn0nn0  13212  xrsupsslem  13274  xrinfmsslem  13275  supxrunb1  13286  supxrunb2  13287  difreicc  13452  elfz0ubfz0  13600  elfz0fzfz0  13601  fz0fzelfz0  13602  fz0fzdiffz0  13605  fzo1fzo0n0  13683  elfzodifsumelfzo  13699  ssfzo12  13727  ssfzo12bi  13729  fzoopth  13730  elfznelfzo  13740  injresinjlem  13755  injresinj  13756  addmodlteq  13918  uzindi  13954  ssnn0fi  13957  suppssfz  13966  facwordi  14261  hasheqf1oi  14323  hashf1rn  14324  fundmge2nop0  14474  swrdswrdlem  14676  swrdswrd  14677  wrd2ind  14695  swrdccatin1  14697  pfxccatin12lem2  14703  swrdccat  14707  reuccatpfxs1lem  14718  repsdf2  14750  cshwidx0  14778  cshweqrep  14793  2cshwcshw  14798  cshwcsh2id  14801  swrdco  14810  wwlktovfo  14931  sqrt2irr  16224  oddnn02np1  16325  oddge22np1  16326  evennn02n  16327  evennn2n  16328  dfgcd2  16523  lcmf  16610  lcmfunsnlem2lem2  16616  initoeu2lem1  17983  symgfix2  19353  gsmsymgreqlem2  19368  psgnunilem4  19434  01eq0ringOLD  20447  lmodfopnelem1  20811  nzerooringczr  21397  cply1mul  22190  gsummoncoe1  22202  mamufacex  22290  matecl  22319  gsummatr01  22553  mp2pm2mplem4  22703  chfacfscmul0  22752  chfacfpmmul0  22756  cayhamlem1  22760  fbunfip  23763  tngngp3  24551  mpomulcn  24765  zabsle1  27214  gausslemma2dlem1a  27283  2lgsoddprm  27334  2sqreunnltblem  27369  umgrnloopv  29040  upgredg2vtx  29075  usgruspgrb  29117  usgrnloopvALT  29135  usgredg2vlem2  29160  edg0usgr  29187  nbuhgr  29277  nbumgr  29281  nbuhgr2vtx1edgblem  29285  cusgredg  29358  cusgrsize2inds  29388  sizusglecusg  29398  umgr2v2enb1  29461  rusgr1vtx  29523  uspgr2wlkeq  29581  wlkreslem  29604  spthonepeq  29689  usgr2trlspth  29698  clwlkl1loop  29720  lfgrn1cycl  29742  uspgrn2crct  29745  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  wwlksnextbi  29831  wwlksnredwwlkn0  29833  wwlksnextinj  29836  wspthsnonn0vne  29854  umgr2adedgspth  29885  umgr2wlk  29886  usgr2wspthons3  29901  clwlkclwwlklem2a1  29928  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwwisshclwws  29951  erclwwlktr  29958  clwwlkn1loopb  29979  clwwlknwwlksnb  29991  clwwlkext2edg  29992  erclwwlkntr  30007  clwwlknon1  30033  clwwlknonwwlknonb  30042  clwwlknonex2lem2  30044  upgr1wlkdlem1  30081  upgr3v3e3cycl  30116  uhgr3cyclex  30118  upgr4cycl4dv4e  30121  eucrctshift  30179  frgr3vlem1  30209  3cyclfrgrrn1  30221  3cyclfrgrrn  30222  4cycl2vnunb  30226  frgrnbnb  30229  frgrncvvdeqlem8  30242  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  frgr2wwlk1  30265  2clwwlk2clwwlk  30286  numclwwlk1lem2fo  30294  frgrreg  30330  friendshipgt3  30334  shmodsi  31325  kbass6  32057  mdsymlem6  32344  mdsymlem7  32345  cdj3lem2a  32372  cdj3lem3a  32375  satfrel  35361  gonarlem  35388  satffunlem1lem1  35396  satffunlem2lem1  35398  satffun  35403  wl-spae  37516  grpomndo  37876  rngoueqz  37941  zerdivemp1x  37948  elpcliN  39894  dflim5  43325  relexpiidm  43700  relexpxpmin  43713  ntrk0kbimka  44035  eel12131  44709  tratrbVD  44857  2uasbanhVD  44907  funressnfv  47048  funbrafv  47163  otiunsndisjX  47284  ssfz12  47319  iccpartgt  47432  iccelpart  47438  iccpartnel  47443  fargshiftf1  47446  sprsymrelfvlem  47495  sprsymrelf1lem  47496  prproropf1olem4  47511  sbcpr  47526  reupr  47527  poprelb  47529  reuopreuprim  47531  fmtno4prmfac  47577  lighneallem4b  47614  lighneal  47616  mogoldbblem  47725  gbegt5  47766  sbgoldbaltlem1  47784  sbgoldbm  47789  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  bgoldbtbnd  47814  grimedg  47939  cycl3grtri  47950  grlimgrtri  47999  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  lidldomn1  48223  2zrngamgm  48237  rngccatidALTV  48264  ringccatidALTV  48298  scmsuppss  48363  ply1mulgsumlem1  48379  lincsumcl  48424  ellcoellss  48428  lindslinindsimp1  48450  lindslinindimp2lem1  48451  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  itschlc0xyqsol1  48759