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  1664  preqsnd  4820  3elpr2eq  4867  propeqop  5481  po2ne  5576  funopg  6559  eldmrexrnb  7077  peano5  7878  f1o2ndf1  8105  suppimacnv  8158  omordi  8539  omeulem1  8555  brecop  8796  isinf  9213  fiint  9274  carduni  9955  dfac5  10100  dfac2b  10102  cofsmo  10241  cfcoflem  10244  domtriomlem  10414  axdc3lem2  10423  nqereu  10902  squeeze0  12109  zmax  12960  elpq  12990  xnn0lenn0nn0  13262  xrsupsslem  13324  xrinfmsslem  13325  supxrunb1  13336  supxrunb2  13337  difreicc  13502  elfz0ubfz0  13651  elfz0fzfz0  13652  fz0fzelfz0  13653  fz0fzdiffz0  13656  fzo1fzo0n0  13735  elfzodifsumelfzo  13751  ssfzo12  13779  ssfzo12bi  13781  fzoopth  13782  elfznelfzo  13793  injresinjlem  13810  injresinj  13811  addmodlteq  13973  uzindi  14009  ssnn0fi  14012  suppssfz  14021  facwordi  14316  hasheqf1oi  14378  hashf1rn  14379  fundmge2nop0  14529  swrdswrdlem  14731  swrdswrd  14732  wrd2ind  14750  swrdccatin1  14752  pfxccatin12lem2  14758  swrdccat  14762  reuccatpfxs1lem  14773  repsdf2  14805  cshwidx0  14833  cshweqrep  14848  2cshwcshw  14852  cshwcsh2id  14855  swrdco  14864  wwlktovfo  14985  sqrt2irr  16295  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  dfgcd2  16594  lcmf  16681  lcmfunsnlem2lem2  16687  initoeu2lem1  18061  symgfix2  19477  gsmsymgreqlem2  19492  psgnunilem4  19558  01eq0ringOLD  20606  lmodfopnelem1  20988  nzerooringczr  21590  cply1mul  22417  gsummoncoe1  22429  mamufacex  22514  matecl  22543  gsummatr01  22777  mp2pm2mplem4  22927  chfacfscmul0  22976  chfacfpmmul0  22980  cayhamlem1  22984  fbunfip  23987  tngngp3  24774  mpomulcn  24987  zabsle1  27418  gausslemma2dlem1a  27487  2lgsoddprm  27538  2sqreunnltblem  27573  umgrnloopv  29365  upgredg2vtx  29400  usgruspgrb  29442  usgrnloopvALT  29460  usgredg2vlem2  29485  edg0usgr  29512  nbuhgr  29602  nbumgr  29606  nbuhgr2vtx1edgblem  29610  cusgredg  29683  cusgrsize2inds  29712  sizusglecusg  29722  umgr2v2enb1  29785  rusgr1vtx  29847  uspgr2wlkeq  29904  wlkreslem  29926  spthonepeq  30010  usgr2trlspth  30019  clwlkl1loop  30041  lfgrn1cycl  30063  uspgrn2crct  30066  crctcshwlkn0lem3  30070  crctcshwlkn0lem5  30072  wwlksnextbi  30152  wwlksnredwwlkn0  30154  wwlksnextinj  30157  wspthsnonn0vne  30175  umgr2adedgspth  30206  umgr2wlk  30207  usgr2wspthons3  30225  clwlkclwwlklem2a1  30252  clwlkclwwlklem2fv2  30256  clwlkclwwlklem2a4  30257  clwlkclwwlklem2a  30258  clwlkclwwlklem2  30260  clwwisshclwws  30275  erclwwlktr  30282  clwwlkn1loopb  30303  clwwlknwwlksnb  30315  clwwlkext2edg  30316  erclwwlkntr  30331  clwwlknon1  30357  clwwlknonwwlknonb  30366  clwwlknonex2lem2  30368  upgr1wlkdlem1  30405  upgr3v3e3cycl  30440  uhgr3cyclex  30442  upgr4cycl4dv4e  30445  eucrctshift  30503  frgr3vlem1  30533  3cyclfrgrrn1  30545  3cyclfrgrrn  30546  4cycl2vnunb  30550  frgrnbnb  30553  frgrncvvdeqlem8  30566  frgrwopreglem5  30581  frgrwopreglem5ALT  30582  frgr2wwlk1  30589  2clwwlk2clwwlk  30610  numclwwlk1lem2fo  30618  frgrreg  30654  friendshipgt3  30658  shmodsi  31650  kbass6  32382  mdsymlem6  32669  mdsymlem7  32670  cdj3lem2a  32697  cdj3lem3a  32700  satfrel  35730  gonarlem  35757  satffunlem1lem1  35765  satffunlem2lem1  35767  satffun  35772  wl-spae  38036  grpomndo  38386  rngoueqz  38451  zerdivemp1x  38458  elpcliN  40529  dflim5  43918  relexpiidm  44292  relexpxpmin  44305  ntrk0kbimka  44627  eel12131  45286  tratrbVD  45434  2uasbanhVD  45484  funressnfv  47635  funbrafv  47750  otiunsndisjX  47871  ssfz12  47906  iccpartgt  48031  iccelpart  48037  iccpartnel  48042  fargshiftf1  48045  sprsymrelfvlem  48094  sprsymrelf1lem  48095  prproropf1olem4  48110  sbcpr  48125  reupr  48126  poprelb  48128  reuopreuprim  48130  fmtno4prmfac  48179  lighneallem4b  48216  lighneal  48218  nprmdvdsfacm1lem2  48228  mogoldbblem  48340  gbegt5  48381  sbgoldbaltlem1  48399  sbgoldbm  48404  bgoldbtbndlem2  48426  bgoldbtbndlem3  48427  bgoldbtbndlem4  48428  bgoldbtbnd  48429  grimedg  48555  cycl3grtri  48567  grlimgrtri  48623  pgnbgreunbgrlem2lem1  48734  pgnbgreunbgrlem2lem2  48735  pgnbgreunbgrlem2lem3  48736  lidldomn1  48851  2zrngamgm  48865  rngccatidALTV  48892  ringccatidALTV  48926  scmsuppss  49002  ply1mulgsumlem1  49017  lincsumcl  49062  ellcoellss  49066  lindslinindsimp1  49088  lindslinindimp2lem1  49089  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251  itschlc0xyqsol1  49397