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  647  an31s  650  3imp31  1110  3imp21  1112  meredith  1639  preqsnd  4792  3elpr2eq  4840  propeqop  5424  po2ne  5521  funopg  6485  eldmrexrnb  6988  fvn0fvelrn  7055  peano5  7760  peano5OLD  7761  f1o2ndf1  7983  suppimacnv  8010  omordi  8417  omeulem1  8433  brecop  8619  isinf  9064  fiint  9119  carduni  9767  dfac5  9912  dfac2b  9914  cofsmo  10053  cfcoflem  10056  domtriomlem  10226  axdc3lem2  10235  nqereu  10713  squeeze0  11906  zmax  12713  elpq  12743  xnn0lenn0nn0  13007  xrsupsslem  13069  xrinfmsslem  13070  supxrunb1  13081  supxrunb2  13082  difreicc  13244  elfz0ubfz0  13388  elfz0fzfz0  13389  fz0fzelfz0  13390  fz0fzdiffz0  13393  fzo1fzo0n0  13466  elfzodifsumelfzo  13481  ssfzo12  13508  ssfzo12bi  13510  elfznelfzo  13520  injresinjlem  13535  injresinj  13536  addmodlteq  13694  uzindi  13730  ssnn0fi  13733  suppssfz  13742  facwordi  14031  hasheqf1oi  14094  hashf1rn  14095  fundmge2nop0  14234  swrdswrdlem  14445  swrdswrd  14446  wrd2ind  14464  swrdccatin1  14466  pfxccatin12lem2  14472  swrdccat  14476  reuccatpfxs1lem  14487  repsdf2  14519  cshwidx0  14547  cshweqrep  14562  2cshwcshw  14566  cshwcsh2id  14569  swrdco  14578  wwlktovfo  14701  sqrt2irr  15986  oddnn02np1  16085  oddge22np1  16086  evennn02n  16087  evennn2n  16088  dfgcd2  16282  lcmf  16366  lcmfunsnlem2lem2  16372  initoeu2lem1  17757  symgfix2  19052  gsmsymgreqlem2  19067  psgnunilem4  19133  lmodfopnelem1  20187  01eq0ring  20571  cply1mul  21493  gsummoncoe1  21503  mamufacex  21566  matecl  21602  gsummatr01  21836  mp2pm2mplem4  21986  chfacfscmul0  22035  chfacfpmmul0  22039  cayhamlem1  22043  fbunfip  23048  tngngp3  23848  zabsle1  26472  gausslemma2dlem1a  26541  2lgsoddprm  26592  2sqreunnltblem  26627  umgrnloopv  27504  upgredg2vtx  27539  usgruspgrb  27579  usgrnloopvALT  27596  usgredg2vlem2  27621  edg0usgr  27648  nbuhgr  27738  nbumgr  27742  nbuhgr2vtx1edgblem  27746  cusgredg  27819  cusgrsize2inds  27848  sizusglecusg  27858  umgr2v2enb1  27921  rusgr1vtx  27983  uspgr2wlkeq  28041  wlkreslem  28065  spthonepeq  28148  usgr2trlspth  28157  clwlkl1loop  28179  lfgrn1cycl  28198  uspgrn2crct  28201  crctcshwlkn0lem3  28205  crctcshwlkn0lem5  28207  wwlksnextbi  28287  wwlksnredwwlkn0  28289  wwlksnextinj  28292  wspthsnonn0vne  28310  umgr2adedgspth  28341  umgr2wlk  28342  usgr2wspthons3  28357  clwlkclwwlklem2a1  28384  clwlkclwwlklem2fv2  28388  clwlkclwwlklem2a4  28389  clwlkclwwlklem2a  28390  clwlkclwwlklem2  28392  clwwisshclwws  28407  erclwwlktr  28414  clwwlkn1loopb  28435  clwwlknwwlksnb  28447  clwwlkext2edg  28448  erclwwlkntr  28463  clwwlknon1  28489  clwwlknonwwlknonb  28498  clwwlknonex2lem2  28500  upgr1wlkdlem1  28537  upgr3v3e3cycl  28572  uhgr3cyclex  28574  upgr4cycl4dv4e  28577  eucrctshift  28635  frgr3vlem1  28665  3cyclfrgrrn1  28677  3cyclfrgrrn  28678  4cycl2vnunb  28682  frgrnbnb  28685  frgrncvvdeqlem8  28698  frgrwopreglem5  28713  frgrwopreglem5ALT  28714  frgr2wwlk1  28721  2clwwlk2clwwlk  28742  numclwwlk1lem2fo  28750  frgrreg  28786  friendshipgt3  28790  shmodsi  29779  kbass6  30511  mdsymlem6  30798  mdsymlem7  30799  cdj3lem2a  30826  cdj3lem3a  30829  satfrel  33357  gonarlem  33384  satffunlem1lem1  33392  satffunlem2lem1  33394  satffun  33399  wl-spae  35708  grpomndo  36061  rngoueqz  36126  zerdivemp1x  36133  elpcliN  37933  relexpiidm  41336  relexpxpmin  41349  ntrk0kbimka  41673  eel12131  42357  tratrbVD  42505  2uasbanhVD  42555  funressnfv  44577  funbrafv  44690  otiunsndisjX  44811  ssfz12  44846  fzoopth  44859  iccpartgt  44919  iccelpart  44925  iccpartnel  44930  fargshiftf1  44933  sprsymrelfvlem  44982  sprsymrelf1lem  44983  prproropf1olem4  44998  sbcpr  45013  reupr  45014  poprelb  45016  reuopreuprim  45018  fmtno4prmfac  45064  lighneallem4b  45101  lighneal  45103  mogoldbblem  45212  gbegt5  45253  sbgoldbaltlem1  45271  sbgoldbm  45276  bgoldbtbndlem2  45298  bgoldbtbndlem3  45299  bgoldbtbndlem4  45300  bgoldbtbnd  45301  isomuspgrlem2b  45321  isomuspgrlem2d  45323  lidldomn1  45519  2zrngamgm  45537  rngccatidALTV  45587  ringccatidALTV  45650  nzerooringczr  45670  scmsuppss  45748  ply1mulgsumlem1  45767  lincsumcl  45812  ellcoellss  45816  lindslinindsimp1  45838  lindslinindimp2lem1  45839  nn0sumshdiglemA  46005  nn0sumshdiglemB  46006  itschlc0xyqsol1  46152