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  649  an31s  652  3imp31  1112  3imp21  1114  meredith  1643  preqsnd  4859  3elpr2eq  4907  propeqop  5507  po2ne  5604  funopg  6582  eldmrexrnb  7093  fvn0fvelrnOLD  7160  peano5  7883  peano5OLD  7884  f1o2ndf1  8107  suppimacnv  8158  omordi  8565  omeulem1  8581  brecop  8803  isinf  9259  isinfOLD  9260  fiint  9323  carduni  9975  dfac5  10122  dfac2b  10124  cofsmo  10263  cfcoflem  10266  domtriomlem  10436  axdc3lem2  10445  nqereu  10923  squeeze0  12116  zmax  12928  elpq  12958  xnn0lenn0nn0  13223  xrsupsslem  13285  xrinfmsslem  13286  supxrunb1  13297  supxrunb2  13298  difreicc  13460  elfz0ubfz0  13604  elfz0fzfz0  13605  fz0fzelfz0  13606  fz0fzdiffz0  13609  fzo1fzo0n0  13682  elfzodifsumelfzo  13697  ssfzo12  13724  ssfzo12bi  13726  elfznelfzo  13736  injresinjlem  13751  injresinj  13752  addmodlteq  13910  uzindi  13946  ssnn0fi  13949  suppssfz  13958  facwordi  14248  hasheqf1oi  14310  hashf1rn  14311  fundmge2nop0  14452  swrdswrdlem  14653  swrdswrd  14654  wrd2ind  14672  swrdccatin1  14674  pfxccatin12lem2  14680  swrdccat  14684  reuccatpfxs1lem  14695  repsdf2  14727  cshwidx0  14755  cshweqrep  14770  2cshwcshw  14775  cshwcsh2id  14778  swrdco  14787  wwlktovfo  14908  sqrt2irr  16191  oddnn02np1  16290  oddge22np1  16291  evennn02n  16292  evennn2n  16293  dfgcd2  16487  lcmf  16569  lcmfunsnlem2lem2  16575  initoeu2lem1  17963  symgfix2  19283  gsmsymgreqlem2  19298  psgnunilem4  19364  01eq0ringOLD  20305  lmodfopnelem1  20507  cply1mul  21817  gsummoncoe1  21827  mamufacex  21890  matecl  21926  gsummatr01  22160  mp2pm2mplem4  22310  chfacfscmul0  22359  chfacfpmmul0  22363  cayhamlem1  22367  fbunfip  23372  tngngp3  24172  zabsle1  26796  gausslemma2dlem1a  26865  2lgsoddprm  26916  2sqreunnltblem  26951  umgrnloopv  28363  upgredg2vtx  28398  usgruspgrb  28438  usgrnloopvALT  28455  usgredg2vlem2  28480  edg0usgr  28507  nbuhgr  28597  nbumgr  28601  nbuhgr2vtx1edgblem  28605  cusgredg  28678  cusgrsize2inds  28707  sizusglecusg  28717  umgr2v2enb1  28780  rusgr1vtx  28842  uspgr2wlkeq  28900  wlkreslem  28923  spthonepeq  29006  usgr2trlspth  29015  clwlkl1loop  29037  lfgrn1cycl  29056  uspgrn2crct  29059  crctcshwlkn0lem3  29063  crctcshwlkn0lem5  29065  wwlksnextbi  29145  wwlksnredwwlkn0  29147  wwlksnextinj  29150  wspthsnonn0vne  29168  umgr2adedgspth  29199  umgr2wlk  29200  usgr2wspthons3  29215  clwlkclwwlklem2a1  29242  clwlkclwwlklem2fv2  29246  clwlkclwwlklem2a4  29247  clwlkclwwlklem2a  29248  clwlkclwwlklem2  29250  clwwisshclwws  29265  erclwwlktr  29272  clwwlkn1loopb  29293  clwwlknwwlksnb  29305  clwwlkext2edg  29306  erclwwlkntr  29321  clwwlknon1  29347  clwwlknonwwlknonb  29356  clwwlknonex2lem2  29358  upgr1wlkdlem1  29395  upgr3v3e3cycl  29430  uhgr3cyclex  29432  upgr4cycl4dv4e  29435  eucrctshift  29493  frgr3vlem1  29523  3cyclfrgrrn1  29535  3cyclfrgrrn  29536  4cycl2vnunb  29540  frgrnbnb  29543  frgrncvvdeqlem8  29556  frgrwopreglem5  29571  frgrwopreglem5ALT  29572  frgr2wwlk1  29579  2clwwlk2clwwlk  29600  numclwwlk1lem2fo  29608  frgrreg  29644  friendshipgt3  29648  shmodsi  30637  kbass6  31369  mdsymlem6  31656  mdsymlem7  31657  cdj3lem2a  31684  cdj3lem3a  31687  satfrel  34353  gonarlem  34380  satffunlem1lem1  34388  satffunlem2lem1  34390  satffun  34395  mpomulcn  35157  wl-spae  36385  grpomndo  36738  rngoueqz  36803  zerdivemp1x  36810  elpcliN  38759  dflim5  42069  relexpiidm  42445  relexpxpmin  42458  ntrk0kbimka  42780  eel12131  43464  tratrbVD  43612  2uasbanhVD  43662  funressnfv  45743  funbrafv  45856  otiunsndisjX  45977  ssfz12  46012  fzoopth  46025  iccpartgt  46085  iccelpart  46091  iccpartnel  46096  fargshiftf1  46099  sprsymrelfvlem  46148  sprsymrelf1lem  46149  prproropf1olem4  46164  sbcpr  46179  reupr  46180  poprelb  46182  reuopreuprim  46184  fmtno4prmfac  46230  lighneallem4b  46267  lighneal  46269  mogoldbblem  46378  gbegt5  46419  sbgoldbaltlem1  46437  sbgoldbm  46442  bgoldbtbndlem2  46464  bgoldbtbndlem3  46465  bgoldbtbndlem4  46466  bgoldbtbnd  46467  isomuspgrlem2b  46487  isomuspgrlem2d  46489  lidldomn1  46813  2zrngamgm  46827  rngccatidALTV  46877  ringccatidALTV  46940  nzerooringczr  46960  scmsuppss  47038  ply1mulgsumlem1  47057  lincsumcl  47102  ellcoellss  47106  lindslinindsimp1  47128  lindslinindimp2lem1  47129  nn0sumshdiglemA  47295  nn0sumshdiglemB  47296  itschlc0xyqsol1  47442