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  657  an31s  660  3imp31  1117  3imp21  1119  meredith  1648  preqsnd  4797  3elpr2eq  4844  propeqop  5455  po2ne  5549  funopg  6526  eldmrexrnb  7040  peano5  7840  f1o2ndf1  8068  suppimacnv  8121  omordi  8498  omeulem1  8514  brecop  8754  isinf  9172  fiint  9234  carduni  9903  dfac5  10049  dfac2b  10051  cofsmo  10189  cfcoflem  10192  domtriomlem  10362  axdc3lem2  10371  nqereu  10850  squeeze0  12057  zmax  12893  elpq  12923  xnn0lenn0nn0  13195  xrsupsslem  13257  xrinfmsslem  13258  supxrunb1  13269  supxrunb2  13270  difreicc  13435  elfz0ubfz0  13584  elfz0fzfz0  13585  fz0fzelfz0  13586  fz0fzdiffz0  13589  fzo1fzo0n0  13668  elfzodifsumelfzo  13684  ssfzo12  13712  ssfzo12bi  13714  fzoopth  13715  elfznelfzo  13726  injresinjlem  13743  injresinj  13744  addmodlteq  13906  uzindi  13942  ssnn0fi  13945  suppssfz  13954  facwordi  14249  hasheqf1oi  14311  hashf1rn  14312  fundmge2nop0  14462  swrdswrdlem  14664  swrdswrd  14665  wrd2ind  14683  swrdccatin1  14685  pfxccatin12lem2  14691  swrdccat  14695  reuccatpfxs1lem  14706  repsdf2  14738  cshwidx0  14766  cshweqrep  14781  2cshwcshw  14785  cshwcsh2id  14788  swrdco  14797  wwlktovfo  14918  sqrt2irr  16214  oddnn02np1  16315  oddge22np1  16316  evennn02n  16317  evennn2n  16318  dfgcd2  16513  lcmf  16600  lcmfunsnlem2lem2  16606  initoeu2lem1  17979  symgfix2  19389  gsmsymgreqlem2  19404  psgnunilem4  19470  01eq0ringOLD  20510  lmodfopnelem1  20895  nzerooringczr  21462  cply1mul  22289  gsummoncoe1  22301  mamufacex  22386  matecl  22415  gsummatr01  22649  mp2pm2mplem4  22799  chfacfscmul0  22848  chfacfpmmul0  22852  cayhamlem1  22856  fbunfip  23859  tngngp3  24646  mpomulcn  24859  zabsle1  27284  gausslemma2dlem1a  27353  2lgsoddprm  27404  2sqreunnltblem  27439  umgrnloopv  29200  upgredg2vtx  29235  usgruspgrb  29277  usgrnloopvALT  29295  usgredg2vlem2  29320  edg0usgr  29347  nbuhgr  29437  nbumgr  29441  nbuhgr2vtx1edgblem  29445  cusgredg  29518  cusgrsize2inds  29547  sizusglecusg  29557  umgr2v2enb1  29620  rusgr1vtx  29682  uspgr2wlkeq  29739  wlkreslem  29761  spthonepeq  29845  usgr2trlspth  29854  clwlkl1loop  29876  lfgrn1cycl  29898  uspgrn2crct  29901  crctcshwlkn0lem3  29905  crctcshwlkn0lem5  29907  wwlksnextbi  29987  wwlksnredwwlkn0  29989  wwlksnextinj  29992  wspthsnonn0vne  30010  umgr2adedgspth  30041  umgr2wlk  30042  usgr2wspthons3  30060  clwlkclwwlklem2a1  30087  clwlkclwwlklem2fv2  30091  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  clwwisshclwws  30110  erclwwlktr  30117  clwwlkn1loopb  30138  clwwlknwwlksnb  30150  clwwlkext2edg  30151  erclwwlkntr  30166  clwwlknon1  30192  clwwlknonwwlknonb  30201  clwwlknonex2lem2  30203  upgr1wlkdlem1  30240  upgr3v3e3cycl  30275  uhgr3cyclex  30277  upgr4cycl4dv4e  30280  eucrctshift  30338  frgr3vlem1  30368  3cyclfrgrrn1  30380  3cyclfrgrrn  30381  4cycl2vnunb  30385  frgrnbnb  30388  frgrncvvdeqlem8  30401  frgrwopreglem5  30416  frgrwopreglem5ALT  30417  frgr2wwlk1  30424  2clwwlk2clwwlk  30445  numclwwlk1lem2fo  30453  frgrreg  30489  friendshipgt3  30493  shmodsi  31485  kbass6  32217  mdsymlem6  32504  mdsymlem7  32505  cdj3lem2a  32532  cdj3lem3a  32535  satfrel  35602  gonarlem  35629  satffunlem1lem1  35637  satffunlem2lem1  35639  satffun  35644  wl-spae  37899  grpomndo  38249  rngoueqz  38314  zerdivemp1x  38321  elpcliN  40392  dflim5  43781  relexpiidm  44155  relexpxpmin  44168  ntrk0kbimka  44490  eel12131  45163  tratrbVD  45311  2uasbanhVD  45361  funressnfv  47513  funbrafv  47628  otiunsndisjX  47749  ssfz12  47784  iccpartgt  47909  iccelpart  47915  iccpartnel  47920  fargshiftf1  47923  sprsymrelfvlem  47972  sprsymrelf1lem  47973  prproropf1olem4  47988  sbcpr  48003  reupr  48004  poprelb  48006  reuopreuprim  48008  fmtno4prmfac  48057  lighneallem4b  48094  lighneal  48096  nprmdvdsfacm1lem2  48106  mogoldbblem  48218  gbegt5  48259  sbgoldbaltlem1  48277  sbgoldbm  48282  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  bgoldbtbndlem4  48306  bgoldbtbnd  48307  grimedg  48433  cycl3grtri  48445  grlimgrtri  48501  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  lidldomn1  48729  2zrngamgm  48743  rngccatidALTV  48770  ringccatidALTV  48804  scmsuppss  48869  ply1mulgsumlem1  48884  lincsumcl  48929  ellcoellss  48933  lindslinindsimp1  48955  lindslinindimp2lem1  48956  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  itschlc0xyqsol1  49264