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  661  an31s  664  3imp31  1123  3imp21  1125  meredith  1660  preqsnd  4816  3elpr2eq  4863  propeqop  5475  po2ne  5569  funopg  6551  eldmrexrnb  7069  peano5  7870  f1o2ndf1  8096  suppimacnv  8149  omordi  8530  omeulem1  8546  brecop  8787  isinf  9205  fiint  9267  carduni  9936  dfac5  10082  dfac2b  10084  cofsmo  10223  cfcoflem  10226  domtriomlem  10396  axdc3lem2  10405  nqereu  10884  squeeze0  12092  zmax  12943  elpq  12973  xnn0lenn0nn0  13245  xrsupsslem  13307  xrinfmsslem  13308  supxrunb1  13319  supxrunb2  13320  difreicc  13485  elfz0ubfz0  13634  elfz0fzfz0  13635  fz0fzelfz0  13636  fz0fzdiffz0  13639  fzo1fzo0n0  13718  elfzodifsumelfzo  13734  ssfzo12  13762  ssfzo12bi  13764  fzoopth  13765  elfznelfzo  13776  injresinjlem  13793  injresinj  13794  addmodlteq  13956  uzindi  13992  ssnn0fi  13995  suppssfz  14004  facwordi  14299  hasheqf1oi  14361  hashf1rn  14362  fundmge2nop0  14512  swrdswrdlem  14714  swrdswrd  14715  wrd2ind  14733  swrdccatin1  14735  pfxccatin12lem2  14741  swrdccat  14745  reuccatpfxs1lem  14756  repsdf2  14788  cshwidx0  14816  cshweqrep  14831  2cshwcshw  14835  cshwcsh2id  14838  swrdco  14847  wwlktovfo  14968  sqrt2irr  16264  oddnn02np1  16365  oddge22np1  16366  evennn02n  16367  evennn2n  16368  dfgcd2  16563  lcmf  16650  lcmfunsnlem2lem2  16656  initoeu2lem1  18030  symgfix2  19439  gsmsymgreqlem2  19454  psgnunilem4  19520  01eq0ringOLD  20560  lmodfopnelem1  20945  nzerooringczr  21512  cply1mul  22339  gsummoncoe1  22351  mamufacex  22436  matecl  22465  gsummatr01  22699  mp2pm2mplem4  22849  chfacfscmul0  22898  chfacfpmmul0  22902  cayhamlem1  22906  fbunfip  23909  tngngp3  24696  mpomulcn  24909  zabsle1  27337  gausslemma2dlem1a  27406  2lgsoddprm  27457  2sqreunnltblem  27492  umgrnloopv  29253  upgredg2vtx  29288  usgruspgrb  29330  usgrnloopvALT  29348  usgredg2vlem2  29373  edg0usgr  29400  nbuhgr  29490  nbumgr  29494  nbuhgr2vtx1edgblem  29498  cusgredg  29571  cusgrsize2inds  29600  sizusglecusg  29610  umgr2v2enb1  29673  rusgr1vtx  29735  uspgr2wlkeq  29792  wlkreslem  29814  spthonepeq  29898  usgr2trlspth  29907  clwlkl1loop  29929  lfgrn1cycl  29951  uspgrn2crct  29954  crctcshwlkn0lem3  29958  crctcshwlkn0lem5  29960  wwlksnextbi  30040  wwlksnredwwlkn0  30042  wwlksnextinj  30045  wspthsnonn0vne  30063  umgr2adedgspth  30094  umgr2wlk  30095  usgr2wspthons3  30113  clwlkclwwlklem2a1  30140  clwlkclwwlklem2fv2  30144  clwlkclwwlklem2a4  30145  clwlkclwwlklem2a  30146  clwlkclwwlklem2  30148  clwwisshclwws  30163  erclwwlktr  30170  clwwlkn1loopb  30191  clwwlknwwlksnb  30203  clwwlkext2edg  30204  erclwwlkntr  30219  clwwlknon1  30245  clwwlknonwwlknonb  30254  clwwlknonex2lem2  30256  upgr1wlkdlem1  30293  upgr3v3e3cycl  30328  uhgr3cyclex  30330  upgr4cycl4dv4e  30333  eucrctshift  30391  frgr3vlem1  30421  3cyclfrgrrn1  30433  3cyclfrgrrn  30434  4cycl2vnunb  30438  frgrnbnb  30441  frgrncvvdeqlem8  30454  frgrwopreglem5  30469  frgrwopreglem5ALT  30470  frgr2wwlk1  30477  2clwwlk2clwwlk  30498  numclwwlk1lem2fo  30506  frgrreg  30542  friendshipgt3  30546  shmodsi  31538  kbass6  32270  mdsymlem6  32557  mdsymlem7  32558  cdj3lem2a  32585  cdj3lem3a  32588  satfrel  35681  gonarlem  35708  satffunlem1lem1  35716  satffunlem2lem1  35718  satffun  35723  wl-spae  37988  grpomndo  38338  rngoueqz  38403  zerdivemp1x  38410  elpcliN  40481  dflim5  43870  relexpiidm  44244  relexpxpmin  44257  ntrk0kbimka  44579  eel12131  45252  tratrbVD  45400  2uasbanhVD  45450  funressnfv  47601  funbrafv  47716  otiunsndisjX  47837  ssfz12  47872  iccpartgt  47997  iccelpart  48003  iccpartnel  48008  fargshiftf1  48011  sprsymrelfvlem  48060  sprsymrelf1lem  48061  prproropf1olem4  48076  sbcpr  48091  reupr  48092  poprelb  48094  reuopreuprim  48096  fmtno4prmfac  48145  lighneallem4b  48182  lighneal  48184  nprmdvdsfacm1lem2  48194  mogoldbblem  48306  gbegt5  48347  sbgoldbaltlem1  48365  sbgoldbm  48370  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  bgoldbtbndlem4  48394  bgoldbtbnd  48395  grimedg  48521  cycl3grtri  48533  grlimgrtri  48589  pgnbgreunbgrlem2lem1  48700  pgnbgreunbgrlem2lem2  48701  pgnbgreunbgrlem2lem3  48702  lidldomn1  48817  2zrngamgm  48831  rngccatidALTV  48858  ringccatidALTV  48892  scmsuppss  48957  ply1mulgsumlem1  48972  lincsumcl  49017  ellcoellss  49021  lindslinindsimp1  49043  lindslinindimp2lem1  49044  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206  itschlc0xyqsol1  49352