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  652  an31s  655  3imp31  1112  3imp21  1114  meredith  1643  preqsnd  4803  3elpr2eq  4850  propeqop  5455  po2ne  5548  funopg  6526  eldmrexrnb  7038  peano5  7837  f1o2ndf1  8065  suppimacnv  8117  omordi  8494  omeulem1  8510  brecop  8750  isinf  9168  fiint  9230  carduni  9896  dfac5  10042  dfac2b  10044  cofsmo  10182  cfcoflem  10185  domtriomlem  10355  axdc3lem2  10364  nqereu  10843  squeeze0  12050  zmax  12886  elpq  12916  xnn0lenn0nn0  13188  xrsupsslem  13250  xrinfmsslem  13251  supxrunb1  13262  supxrunb2  13263  difreicc  13428  elfz0ubfz0  13577  elfz0fzfz0  13578  fz0fzelfz0  13579  fz0fzdiffz0  13582  fzo1fzo0n0  13661  elfzodifsumelfzo  13677  ssfzo12  13705  ssfzo12bi  13707  fzoopth  13708  elfznelfzo  13719  injresinjlem  13736  injresinj  13737  addmodlteq  13899  uzindi  13935  ssnn0fi  13938  suppssfz  13947  facwordi  14242  hasheqf1oi  14304  hashf1rn  14305  fundmge2nop0  14455  swrdswrdlem  14657  swrdswrd  14658  wrd2ind  14676  swrdccatin1  14678  pfxccatin12lem2  14684  swrdccat  14688  reuccatpfxs1lem  14699  repsdf2  14731  cshwidx0  14759  cshweqrep  14774  2cshwcshw  14778  cshwcsh2id  14781  swrdco  14790  wwlktovfo  14911  sqrt2irr  16207  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  dfgcd2  16506  lcmf  16593  lcmfunsnlem2lem2  16599  initoeu2lem1  17972  symgfix2  19382  gsmsymgreqlem2  19397  psgnunilem4  19463  01eq0ringOLD  20499  lmodfopnelem1  20884  nzerooringczr  21470  cply1mul  22271  gsummoncoe1  22283  mamufacex  22371  matecl  22400  gsummatr01  22634  mp2pm2mplem4  22784  chfacfscmul0  22833  chfacfpmmul0  22837  cayhamlem1  22841  fbunfip  23844  tngngp3  24631  mpomulcn  24844  zabsle1  27273  gausslemma2dlem1a  27342  2lgsoddprm  27393  2sqreunnltblem  27428  umgrnloopv  29189  upgredg2vtx  29224  usgruspgrb  29266  usgrnloopvALT  29284  usgredg2vlem2  29309  edg0usgr  29336  nbuhgr  29426  nbumgr  29430  nbuhgr2vtx1edgblem  29434  cusgredg  29507  cusgrsize2inds  29537  sizusglecusg  29547  umgr2v2enb1  29610  rusgr1vtx  29672  uspgr2wlkeq  29729  wlkreslem  29751  spthonepeq  29835  usgr2trlspth  29844  clwlkl1loop  29866  lfgrn1cycl  29888  uspgrn2crct  29891  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  wwlksnextbi  29977  wwlksnredwwlkn0  29979  wwlksnextinj  29982  wspthsnonn0vne  30000  umgr2adedgspth  30031  umgr2wlk  30032  usgr2wspthons3  30050  clwlkclwwlklem2a1  30077  clwlkclwwlklem2fv2  30081  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwwisshclwws  30100  erclwwlktr  30107  clwwlkn1loopb  30128  clwwlknwwlksnb  30140  clwwlkext2edg  30141  erclwwlkntr  30156  clwwlknon1  30182  clwwlknonwwlknonb  30191  clwwlknonex2lem2  30193  upgr1wlkdlem1  30230  upgr3v3e3cycl  30265  uhgr3cyclex  30267  upgr4cycl4dv4e  30270  eucrctshift  30328  frgr3vlem1  30358  3cyclfrgrrn1  30370  3cyclfrgrrn  30371  4cycl2vnunb  30375  frgrnbnb  30378  frgrncvvdeqlem8  30391  frgrwopreglem5  30406  frgrwopreglem5ALT  30407  frgr2wwlk1  30414  2clwwlk2clwwlk  30435  numclwwlk1lem2fo  30443  frgrreg  30479  friendshipgt3  30483  shmodsi  31475  kbass6  32207  mdsymlem6  32494  mdsymlem7  32495  cdj3lem2a  32522  cdj3lem3a  32525  satfrel  35565  gonarlem  35592  satffunlem1lem1  35600  satffunlem2lem1  35602  satffun  35607  wl-spae  37860  grpomndo  38210  rngoueqz  38275  zerdivemp1x  38282  elpcliN  40353  dflim5  43775  relexpiidm  44149  relexpxpmin  44162  ntrk0kbimka  44484  eel12131  45157  tratrbVD  45305  2uasbanhVD  45355  funressnfv  47503  funbrafv  47618  otiunsndisjX  47739  ssfz12  47774  iccpartgt  47899  iccelpart  47905  iccpartnel  47910  fargshiftf1  47913  sprsymrelfvlem  47962  sprsymrelf1lem  47963  prproropf1olem4  47978  sbcpr  47993  reupr  47994  poprelb  47996  reuopreuprim  47998  fmtno4prmfac  48047  lighneallem4b  48084  lighneal  48086  nprmdvdsfacm1lem2  48096  mogoldbblem  48208  gbegt5  48249  sbgoldbaltlem1  48267  sbgoldbm  48272  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  grimedg  48423  cycl3grtri  48435  grlimgrtri  48491  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  lidldomn1  48719  2zrngamgm  48733  rngccatidALTV  48760  ringccatidALTV  48794  scmsuppss  48859  ply1mulgsumlem1  48874  lincsumcl  48919  ellcoellss  48923  lindslinindsimp1  48945  lindslinindimp2lem1  48946  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  itschlc0xyqsol1  49254