Theorem com13 89

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 88	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com23 87	1 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com24  96  an13s  664  an31s  667  3imp31  1129  3imp21  1131  meredith  1674  preqsnd  4822  3elpr2eq  4869  propeqop  5488  po2ne  5583  funopg  6571  eldmrexrnb  7089  peano5  7894  f1o2ndf1  8123  suppimacnv  8176  omordi  8557  omeulem1  8573  brecop  8814  isinf  9239  fiint  9300  carduni  9990  dfac5  10135  dfac2b  10137  cofsmo  10275  cfcoflem  10278  domtriomlem  10448  axdc3lem2  10457  nqereu  10942  squeeze0  12146  zmax  12998  elpq  13029  xnn0lenn0nn0  13301  xrsupsslem  13363  xrinfmsslem  13364  supxrunb1  13375  supxrunb2  13376  difreicc  13541  elfz0ubfz0  13691  elfz0fzfz0  13692  fz0fzelfz0  13693  fz0fzdiffz0  13696  fzo1fzo0n0  13775  elfzodifsumelfzo  13791  ssfzo12  13819  ssfzo12bi  13821  fzoopth  13822  elfznelfzo  13833  injresinjlem  13850  injresinj  13851  addmodlteq  14014  uzindi  14050  ssnn0fi  14053  suppssfz  14062  facwordi  14357  hasheqf1oi  14419  hashf1rn  14420  fundmge2nop0  14571  swrdswrdlem  14777  swrdswrd  14778  wrd2ind  14796  swrdccatin1  14798  pfxccatin12lem2  14804  swrdccat  14808  reuccatpfxs1lem  14819  repsdf2  14853  cshwidx0  14881  cshweqrep  14896  2cshwcshw  14900  cshwcsh2id  14903  swrdco  14912  wwlktovfo  15035  sqrt2irr  16343  oddnn02np1  16444  oddge22np1  16445  evennn02n  16446  evennn2n  16447  dfgcd2  16642  lcmf  16729  lcmfunsnlem2lem2  16735  initoeu2lem1  18109  symgfix2  19549  gsmsymgreqlem2  19564  psgnunilem4  19630  01eq0ringOLD  20698  lmodfopnelem1  21088  nzerooringczr  21699  cply1mul  22527  gsummoncoe1  22539  mamufacex  22624  matecl  22653  gsummatr01  22887  mp2pm2mplem4  23040  chfacfscmul0  23089  chfacfpmmul0  23093  cayhamlem1  23097  fbunfip  24101  tngngp3  24888  mpomulcn  25101  zabsle1  27540  gausslemma2dlem1a  27609  2lgsoddprm  27660  2sqreunnltblem  27695  umgrnloopv  29571  upgredg2vtx  29606  usgruspgrb  29651  usgrnloopvALT  29669  usgredg2vlem2  29694  edg0usgr  29721  nbuhgr  29811  nbumgr  29815  nbuhgr2vtx1edgblem  29819  cusgredg  29892  cusgrsize2inds  29921  sizusglecusg  29931  umgr2v2enb1  29994  rusgr1vtx  30056  uspgr2wlkeq  30113  wlkreslem  30135  spthonepeq  30225  usgr2trlspth  30234  clwlkl1loop  30257  lfgrn1cycl  30281  uspgrn2crct  30284  crctcshwlkn0lem3  30288  crctcshwlkn0lem5  30290  wwlksnextbi  30370  wwlksnredwwlkn0  30372  wwlksnextinj  30375  wspthsnonn0vne  30393  umgr2adedgspth  30424  umgr2wlk  30425  usgr2wspthons3  30443  clwlkclwwlklem2a1  30470  clwlkclwwlklem2fv2  30474  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwwisshclwws  30493  erclwwlktr  30500  clwwlkn1loopb  30521  clwwlknwwlksnb  30533  clwwlkext2edg  30534  erclwwlkntr  30549  clwwlknon1  30575  clwwlknonwwlknonb  30584  clwwlknonex2lem2  30586  upgr1wlkdlem1  30623  upgr3v3e3cycl  30668  uhgr3cyclex  30670  upgr4cycl4dv4e  30673  eucrctshift  30731  frgr3vlem1  30761  3cyclfrgrrn1  30773  3cyclfrgrrn  30774  4cycl2vnunb  30778  frgrnbnb  30781  frgrncvvdeqlem8  30794  frgrwopreglem5  30809  frgrwopreglem5ALT  30810  frgr2wwlk1  30817  2clwwlk2clwwlk  30838  numclwwlk1lem2fo  30846  frgrreg  30882  friendshipgt3  30886  shmodsi  31878  kbass6  32610  mdsymlem6  32897  mdsymlem7  32898  cdj3lem2a  32925  cdj3lem3a  32928  satfrel  35954  gonarlem  35981  satffunlem1lem1  35989  satffunlem2lem1  35991  satffun  35996  wl-spae  38292  grpomndo  38633  rngoueqz  38698  zerdivemp1x  38705  elpcliN  40774  dflim5  44178  relexpiidm  44552  relexpxpmin  44565  ntrk0kbimka  44887  eel12131  45543  tratrbVD  45691  2uasbanhVD  45741  funressnfv  47939  funbrafv  48054  otiunsndisjX  48175  ssfz12  48210  iccpartgt  48335  iccelpart  48341  iccpartnel  48346  fargshiftf1  48349  sprsymrelfvlem  48398  sprsymrelf1lem  48399  prproropf1olem4  48414  sbcpr  48429  reupr  48430  poprelb  48432  reuopreuprim  48434  fmtno4prmfac  48483  lighneallem4b  48520  lighneal  48522  nprmdvdsfacm1lem2  48532  mogoldbblem  48644  gbegt5  48685  sbgoldbaltlem1  48703  sbgoldbm  48708  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbndlem4  48732  bgoldbtbnd  48733  grimedg  48859  cycl3grtri  48871  grlimgrtri  48927  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  lidldomn1  49154  2zrngamgm  49168  rngccatidALTV  49195  ringccatidALTV  49229  scmsuppss  49309  ply1mulgsumlem1  49324  lincsumcl  49369  ellcoellss  49373  lindslinindsimp1  49395  lindslinindimp2lem1  49396  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  itschlc0xyqsol1  49704