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  4815  3elpr2eq  4862  propeqop  5455  po2ne  5548  funopg  6526  eldmrexrnb  7037  peano5  7835  f1o2ndf1  8064  suppimacnv  8116  omordi  8493  omeulem1  8509  brecop  8747  isinf  9165  fiint  9227  carduni  9893  dfac5  10039  dfac2b  10041  cofsmo  10179  cfcoflem  10182  domtriomlem  10352  axdc3lem2  10361  nqereu  10840  squeeze0  12045  zmax  12858  elpq  12888  xnn0lenn0nn0  13160  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  supxrunb2  13235  difreicc  13400  elfz0ubfz0  13548  elfz0fzfz0  13549  fz0fzelfz0  13550  fz0fzdiffz0  13553  fzo1fzo0n0  13631  elfzodifsumelfzo  13647  ssfzo12  13675  ssfzo12bi  13677  fzoopth  13678  elfznelfzo  13689  injresinjlem  13706  injresinj  13707  addmodlteq  13869  uzindi  13905  ssnn0fi  13908  suppssfz  13917  facwordi  14212  hasheqf1oi  14274  hashf1rn  14275  fundmge2nop0  14425  swrdswrdlem  14627  swrdswrd  14628  wrd2ind  14646  swrdccatin1  14648  pfxccatin12lem2  14654  swrdccat  14658  reuccatpfxs1lem  14669  repsdf2  14701  cshwidx0  14729  cshweqrep  14744  2cshwcshw  14748  cshwcsh2id  14751  swrdco  14760  wwlktovfo  14881  sqrt2irr  16174  oddnn02np1  16275  oddge22np1  16276  evennn02n  16277  evennn2n  16278  dfgcd2  16473  lcmf  16560  lcmfunsnlem2lem2  16566  initoeu2lem1  17938  symgfix2  19345  gsmsymgreqlem2  19360  psgnunilem4  19426  01eq0ringOLD  20464  lmodfopnelem1  20849  nzerooringczr  21435  cply1mul  22240  gsummoncoe1  22252  mamufacex  22340  matecl  22369  gsummatr01  22603  mp2pm2mplem4  22753  chfacfscmul0  22802  chfacfpmmul0  22806  cayhamlem1  22810  fbunfip  23813  tngngp3  24600  mpomulcn  24814  zabsle1  27263  gausslemma2dlem1a  27332  2lgsoddprm  27383  2sqreunnltblem  27418  umgrnloopv  29179  upgredg2vtx  29214  usgruspgrb  29256  usgrnloopvALT  29274  usgredg2vlem2  29299  edg0usgr  29326  nbuhgr  29416  nbumgr  29420  nbuhgr2vtx1edgblem  29424  cusgredg  29497  cusgrsize2inds  29527  sizusglecusg  29537  umgr2v2enb1  29600  rusgr1vtx  29662  uspgr2wlkeq  29719  wlkreslem  29741  spthonepeq  29825  usgr2trlspth  29834  clwlkl1loop  29856  lfgrn1cycl  29878  uspgrn2crct  29881  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  wwlksnextbi  29967  wwlksnredwwlkn0  29969  wwlksnextinj  29972  wspthsnonn0vne  29990  umgr2adedgspth  30021  umgr2wlk  30022  usgr2wspthons3  30040  clwlkclwwlklem2a1  30067  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwwisshclwws  30090  erclwwlktr  30097  clwwlkn1loopb  30118  clwwlknwwlksnb  30130  clwwlkext2edg  30131  erclwwlkntr  30146  clwwlknon1  30172  clwwlknonwwlknonb  30181  clwwlknonex2lem2  30183  upgr1wlkdlem1  30220  upgr3v3e3cycl  30255  uhgr3cyclex  30257  upgr4cycl4dv4e  30260  eucrctshift  30318  frgr3vlem1  30348  3cyclfrgrrn1  30360  3cyclfrgrrn  30361  4cycl2vnunb  30365  frgrnbnb  30368  frgrncvvdeqlem8  30381  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  frgr2wwlk1  30404  2clwwlk2clwwlk  30425  numclwwlk1lem2fo  30433  frgrreg  30469  friendshipgt3  30473  shmodsi  31464  kbass6  32196  mdsymlem6  32483  mdsymlem7  32484  cdj3lem2a  32511  cdj3lem3a  32514  satfrel  35561  gonarlem  35588  satffunlem1lem1  35596  satffunlem2lem1  35598  satffun  35603  wl-spae  37726  grpomndo  38076  rngoueqz  38141  zerdivemp1x  38148  elpcliN  40153  dflim5  43571  relexpiidm  43945  relexpxpmin  43958  ntrk0kbimka  44280  eel12131  44953  tratrbVD  45101  2uasbanhVD  45151  funressnfv  47289  funbrafv  47404  otiunsndisjX  47525  ssfz12  47560  iccpartgt  47673  iccelpart  47679  iccpartnel  47684  fargshiftf1  47687  sprsymrelfvlem  47736  sprsymrelf1lem  47737  prproropf1olem4  47752  sbcpr  47767  reupr  47768  poprelb  47770  reuopreuprim  47772  fmtno4prmfac  47818  lighneallem4b  47855  lighneal  47857  mogoldbblem  47966  gbegt5  48007  sbgoldbaltlem1  48025  sbgoldbm  48030  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  grimedg  48181  cycl3grtri  48193  grlimgrtri  48249  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  lidldomn1  48477  2zrngamgm  48491  rngccatidALTV  48518  ringccatidALTV  48552  scmsuppss  48617  ply1mulgsumlem1  48632  lincsumcl  48677  ellcoellss  48681  lindslinindsimp1  48703  lindslinindimp2lem1  48704  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  itschlc0xyqsol1  49012