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  651  an31s  654  3imp31  1111  3imp21  1113  meredith  1641  preqsnd  4810  3elpr2eq  4857  propeqop  5450  po2ne  5543  funopg  6516  eldmrexrnb  7026  fvn0fvelrnOLD  7097  peano5  7826  f1o2ndf1  8055  suppimacnv  8107  omordi  8484  omeulem1  8500  brecop  8737  isinf  9154  fiint  9216  fiintOLD  9217  carduni  9877  dfac5  10023  dfac2b  10025  cofsmo  10163  cfcoflem  10166  domtriomlem  10336  axdc3lem2  10345  nqereu  10823  squeeze0  12028  zmax  12846  elpq  12876  xnn0lenn0nn0  13147  xrsupsslem  13209  xrinfmsslem  13210  supxrunb1  13221  supxrunb2  13222  difreicc  13387  elfz0ubfz0  13535  elfz0fzfz0  13536  fz0fzelfz0  13537  fz0fzdiffz0  13540  fzo1fzo0n0  13618  elfzodifsumelfzo  13634  ssfzo12  13662  ssfzo12bi  13664  fzoopth  13665  elfznelfzo  13675  injresinjlem  13690  injresinj  13691  addmodlteq  13853  uzindi  13889  ssnn0fi  13892  suppssfz  13901  facwordi  14196  hasheqf1oi  14258  hashf1rn  14259  fundmge2nop0  14409  swrdswrdlem  14610  swrdswrd  14611  wrd2ind  14629  swrdccatin1  14631  pfxccatin12lem2  14637  swrdccat  14641  reuccatpfxs1lem  14652  repsdf2  14684  cshwidx0  14712  cshweqrep  14727  2cshwcshw  14732  cshwcsh2id  14735  swrdco  14744  wwlktovfo  14865  sqrt2irr  16158  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  dfgcd2  16457  lcmf  16544  lcmfunsnlem2lem2  16550  initoeu2lem1  17921  symgfix2  19295  gsmsymgreqlem2  19310  psgnunilem4  19376  01eq0ringOLD  20416  lmodfopnelem1  20801  nzerooringczr  21387  cply1mul  22181  gsummoncoe1  22193  mamufacex  22281  matecl  22310  gsummatr01  22544  mp2pm2mplem4  22694  chfacfscmul0  22743  chfacfpmmul0  22747  cayhamlem1  22751  fbunfip  23754  tngngp3  24542  mpomulcn  24756  zabsle1  27205  gausslemma2dlem1a  27274  2lgsoddprm  27325  2sqreunnltblem  27360  umgrnloopv  29051  upgredg2vtx  29086  usgruspgrb  29128  usgrnloopvALT  29146  usgredg2vlem2  29171  edg0usgr  29198  nbuhgr  29288  nbumgr  29292  nbuhgr2vtx1edgblem  29296  cusgredg  29369  cusgrsize2inds  29399  sizusglecusg  29409  umgr2v2enb1  29472  rusgr1vtx  29534  uspgr2wlkeq  29591  wlkreslem  29613  spthonepeq  29697  usgr2trlspth  29706  clwlkl1loop  29728  lfgrn1cycl  29750  uspgrn2crct  29753  crctcshwlkn0lem3  29757  crctcshwlkn0lem5  29759  wwlksnextbi  29839  wwlksnredwwlkn0  29841  wwlksnextinj  29844  wspthsnonn0vne  29862  umgr2adedgspth  29893  umgr2wlk  29894  usgr2wspthons3  29909  clwlkclwwlklem2a1  29936  clwlkclwwlklem2fv2  29940  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwwisshclwws  29959  erclwwlktr  29966  clwwlkn1loopb  29987  clwwlknwwlksnb  29999  clwwlkext2edg  30000  erclwwlkntr  30015  clwwlknon1  30041  clwwlknonwwlknonb  30050  clwwlknonex2lem2  30052  upgr1wlkdlem1  30089  upgr3v3e3cycl  30124  uhgr3cyclex  30126  upgr4cycl4dv4e  30129  eucrctshift  30187  frgr3vlem1  30217  3cyclfrgrrn1  30229  3cyclfrgrrn  30230  4cycl2vnunb  30234  frgrnbnb  30237  frgrncvvdeqlem8  30250  frgrwopreglem5  30265  frgrwopreglem5ALT  30266  frgr2wwlk1  30273  2clwwlk2clwwlk  30294  numclwwlk1lem2fo  30302  frgrreg  30338  friendshipgt3  30342  shmodsi  31333  kbass6  32065  mdsymlem6  32352  mdsymlem7  32353  cdj3lem2a  32380  cdj3lem3a  32383  satfrel  35340  gonarlem  35367  satffunlem1lem1  35375  satffunlem2lem1  35377  satffun  35382  wl-spae  37495  grpomndo  37855  rngoueqz  37920  zerdivemp1x  37927  elpcliN  39872  dflim5  43302  relexpiidm  43677  relexpxpmin  43690  ntrk0kbimka  44012  eel12131  44686  tratrbVD  44834  2uasbanhVD  44884  funressnfv  47027  funbrafv  47142  otiunsndisjX  47263  ssfz12  47298  iccpartgt  47411  iccelpart  47417  iccpartnel  47422  fargshiftf1  47425  sprsymrelfvlem  47474  sprsymrelf1lem  47475  prproropf1olem4  47490  sbcpr  47505  reupr  47506  poprelb  47508  reuopreuprim  47510  fmtno4prmfac  47556  lighneallem4b  47593  lighneal  47595  mogoldbblem  47704  gbegt5  47745  sbgoldbaltlem1  47763  sbgoldbm  47768  bgoldbtbndlem2  47790  bgoldbtbndlem3  47791  bgoldbtbndlem4  47792  bgoldbtbnd  47793  grimedg  47919  cycl3grtri  47931  grlimgrtri  47987  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  lidldomn1  48215  2zrngamgm  48229  rngccatidALTV  48256  ringccatidALTV  48290  scmsuppss  48355  ply1mulgsumlem1  48371  lincsumcl  48416  ellcoellss  48420  lindslinindsimp1  48442  lindslinindimp2lem1  48443  nn0sumshdiglemA  48604  nn0sumshdiglemB  48605  itschlc0xyqsol1  48751