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	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
com13	|- ( ch -> ( ps -> ( ph -> th ) ) )

Proof of Theorem com13

Step	Hyp	Ref	Expression
1		com3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com3r 87	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com23 86	1 |- ( ch -> ( ps -> ( ph -> th ) ) )

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  imim12  105  an13s  845  an31s  848  3imp31  1257  meredith  1566  3elpr2eq  4435  propeqop  4970  predpo  5698  funopg  5922  eldmrexrnb  6366  fvn0fvelrn  6430  peano5  7089  f1o2ndf1  7285  suppimacnv  7306  omordi  7646  omeulem1  7662  brecop  7840  isinf  8173  fiint  8237  carduni  8807  dfac5  8951  dfac2  8953  cofsmo  9091  cfcoflem  9094  domtriomlem  9264  axdc3lem2  9273  nqereu  9751  squeeze0  10926  zmax  11785  xnn0lenn0nn0  12075  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  supxrunb2  12150  difreicc  12304  elfz0ubfz0  12443  elfz0fzfz0  12444  fz0fzelfz0  12445  fz0fzdiffz0  12448  fzo1fzo0n0  12518  elfzodifsumelfzo  12533  ssfzo12  12561  ssfzo12bi  12563  elfznelfzo  12573  injresinjlem  12588  injresinj  12589  addmodlteq  12745  uzindi  12781  ssnn0fi  12784  suppssfz  12794  facwordi  13076  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashf1rn  13142  hashf1rnOLD  13143  hash2prde  13252  fundmge2nop0  13274  swrdswrdlem  13459  swrdswrd  13460  wrd2ind  13477  reuccats1lem  13479  swrdccatin1  13483  swrdccatin12lem2  13489  swrdccat  13493  repsdf2  13525  cshwidx0  13552  cshweqrep  13567  2cshwcshw  13571  cshwcsh2id  13574  swrdco  13583  wwlktovfo  13701  sqrt2irr  14979  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  dfgcd2  15263  lcmf  15346  lcmfunsnlem2lem2  15352  initoeu2lem1  16664  symgfix2  17836  gsmsymgreqlem2  17851  psgnunilem4  17917  lmodfopnelem1  18899  01eq0ring  19272  cply1mul  19664  gsummoncoe1  19674  mamufacex  20195  matecl  20231  gsummatr01lem4  20464  gsummatr01  20465  mp2pm2mplem4  20614  chfacfscmul0  20663  chfacfpmmul0  20667  cayhamlem1  20671  fbunfip  21673  tngngp3  22460  zabsle1  25021  gausslemma2dlem1a  25090  2lgsoddprm  25141  umgrnloopv  26001  upgredg2vtx  26036  usgruspgrb  26076  usgrnloopvALT  26093  usgredg2vlem2  26118  edg0usgr  26145  nbuhgr  26239  nbumgr  26243  nbuhgr2vtx1edgblem  26247  cusgredg  26320  cusgrsize2inds  26349  sizusglecusg  26359  umgr2v2enb1  26422  rusgr1vtx  26484  upgrewlkle2  26502  uspgr2wlkeq  26542  wlkreslem  26566  spthonepeq  26648  usgr2trlspth  26657  usgr2pth  26660  clwlkl1loop  26678  lfgrn1cycl  26697  uspgrn2crct  26700  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  wwlksnextbi  26789  wwlksnredwwlkn0  26791  wwlksnextinj  26794  wspthsnonn0vne  26813  umgr2adedgspth  26844  umgr2wlk  26845  usgr2wspthons3  26857  clwlkclwwlklem2a1  26893  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlksext2edg  26923  clwwisshclwws  26928  erclwwlkstr  26936  erclwwlksntr  26948  upgr1wlkdlem1  27005  upgr3v3e3cycl  27040  uhgr3cyclex  27042  upgr4cycl4dv4e  27045  eucrctshift  27103  frgr3vlem1  27137  3cyclfrgrrn1  27149  3cyclfrgrrn  27150  4cycl2vnunb  27154  frgrnbnb  27157  frgrncvvdeqlem8  27170  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  frgr2wwlk1  27193  numclwwlkffin0  27215  numclwlk1lem2fo  27228  frgrreg  27252  friendshipgt3  27256  shmodsi  28248  kbass6  28980  mdsymlem6  29267  mdsymlem7  29268  cdj3lem2a  29295  cdj3lem3a  29298  bj-snmoore  33068  wl-spae  33306  grpomndo  33674  rngoueqz  33739  zerdivemp1x  33746  elpcliN  35179  relexpiidm  37996  relexpxpmin  38009  ntrk0kbimka  38337  eel12131  38938  tratrbVD  39097  2uasbanhVD  39147  funressnfv  41208  funbrafv  41238  otiunsndisjX  41298  ssfz12  41324  fzoopth  41337  iccpartgt  41363  iccelpart  41369  iccpartnel  41374  fargshiftf1  41377  pfxccatin12lem2  41424  reuccatpfxs1lem  41433  reuccatpfxs1  41434  fmtno4prmfac  41484  lighneallem4b  41526  lighneal  41528  mogoldbblem  41629  gbegt5  41649  sbgoldbaltlem1  41667  sbgoldbm  41672  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  sprsymrelfvlem  41740  sprsymrelf1lem  41741  lidldomn1  41921  2zrngamgm  41939  rngccatidALTV  41989  ringccatidALTV  42052  nzerooringczr  42072  scmsuppss  42153  ply1mulgsumlem1  42174  lincsumcl  42220  ellcoellss  42224  lindslinindsimp1  42246  lindslinindimp2lem1  42247  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414