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  4813  3elpr2eq  4860  propeqop  5454  po2ne  5547  funopg  6520  eldmrexrnb  7030  fvn0fvelrnOLD  7101  peano5  7833  f1o2ndf1  8062  suppimacnv  8114  omordi  8491  omeulem1  8507  brecop  8744  isinf  9165  isinfOLD  9166  fiint  9235  fiintOLD  9236  carduni  9896  dfac5  10042  dfac2b  10044  cofsmo  10182  cfcoflem  10185  domtriomlem  10355  axdc3lem2  10364  nqereu  10842  squeeze0  12046  zmax  12864  elpq  12894  xnn0lenn0nn0  13165  xrsupsslem  13227  xrinfmsslem  13228  supxrunb1  13239  supxrunb2  13240  difreicc  13405  elfz0ubfz0  13553  elfz0fzfz0  13554  fz0fzelfz0  13555  fz0fzdiffz0  13558  fzo1fzo0n0  13636  elfzodifsumelfzo  13652  ssfzo12  13680  ssfzo12bi  13682  fzoopth  13683  elfznelfzo  13693  injresinjlem  13708  injresinj  13709  addmodlteq  13871  uzindi  13907  ssnn0fi  13910  suppssfz  13919  facwordi  14214  hasheqf1oi  14276  hashf1rn  14277  fundmge2nop0  14427  swrdswrdlem  14628  swrdswrd  14629  wrd2ind  14647  swrdccatin1  14649  pfxccatin12lem2  14655  swrdccat  14659  reuccatpfxs1lem  14670  repsdf2  14702  cshwidx0  14730  cshweqrep  14745  2cshwcshw  14750  cshwcsh2id  14753  swrdco  14762  wwlktovfo  14883  sqrt2irr  16176  oddnn02np1  16277  oddge22np1  16278  evennn02n  16279  evennn2n  16280  dfgcd2  16475  lcmf  16562  lcmfunsnlem2lem2  16568  initoeu2lem1  17939  symgfix2  19313  gsmsymgreqlem2  19328  psgnunilem4  19394  01eq0ringOLD  20434  lmodfopnelem1  20819  nzerooringczr  21405  cply1mul  22199  gsummoncoe1  22211  mamufacex  22299  matecl  22328  gsummatr01  22562  mp2pm2mplem4  22712  chfacfscmul0  22761  chfacfpmmul0  22765  cayhamlem1  22769  fbunfip  23772  tngngp3  24560  mpomulcn  24774  zabsle1  27223  gausslemma2dlem1a  27292  2lgsoddprm  27343  2sqreunnltblem  27378  umgrnloopv  29069  upgredg2vtx  29104  usgruspgrb  29146  usgrnloopvALT  29164  usgredg2vlem2  29189  edg0usgr  29216  nbuhgr  29306  nbumgr  29310  nbuhgr2vtx1edgblem  29314  cusgredg  29387  cusgrsize2inds  29417  sizusglecusg  29427  umgr2v2enb1  29490  rusgr1vtx  29552  uspgr2wlkeq  29609  wlkreslem  29631  spthonepeq  29715  usgr2trlspth  29724  clwlkl1loop  29746  lfgrn1cycl  29768  uspgrn2crct  29771  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  wwlksnextbi  29857  wwlksnredwwlkn0  29859  wwlksnextinj  29862  wspthsnonn0vne  29880  umgr2adedgspth  29911  umgr2wlk  29912  usgr2wspthons3  29927  clwlkclwwlklem2a1  29954  clwlkclwwlklem2fv2  29958  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwwisshclwws  29977  erclwwlktr  29984  clwwlkn1loopb  30005  clwwlknwwlksnb  30017  clwwlkext2edg  30018  erclwwlkntr  30033  clwwlknon1  30059  clwwlknonwwlknonb  30068  clwwlknonex2lem2  30070  upgr1wlkdlem1  30107  upgr3v3e3cycl  30142  uhgr3cyclex  30144  upgr4cycl4dv4e  30147  eucrctshift  30205  frgr3vlem1  30235  3cyclfrgrrn1  30247  3cyclfrgrrn  30248  4cycl2vnunb  30252  frgrnbnb  30255  frgrncvvdeqlem8  30268  frgrwopreglem5  30283  frgrwopreglem5ALT  30284  frgr2wwlk1  30291  2clwwlk2clwwlk  30312  numclwwlk1lem2fo  30320  frgrreg  30356  friendshipgt3  30360  shmodsi  31351  kbass6  32083  mdsymlem6  32370  mdsymlem7  32371  cdj3lem2a  32398  cdj3lem3a  32401  satfrel  35342  gonarlem  35369  satffunlem1lem1  35377  satffunlem2lem1  35379  satffun  35384  wl-spae  37497  grpomndo  37857  rngoueqz  37922  zerdivemp1x  37929  elpcliN  39875  dflim5  43305  relexpiidm  43680  relexpxpmin  43693  ntrk0kbimka  44015  eel12131  44689  tratrbVD  44837  2uasbanhVD  44887  funressnfv  47031  funbrafv  47146  otiunsndisjX  47267  ssfz12  47302  iccpartgt  47415  iccelpart  47421  iccpartnel  47426  fargshiftf1  47429  sprsymrelfvlem  47478  sprsymrelf1lem  47479  prproropf1olem4  47494  sbcpr  47509  reupr  47510  poprelb  47512  reuopreuprim  47514  fmtno4prmfac  47560  lighneallem4b  47597  lighneal  47599  mogoldbblem  47708  gbegt5  47749  sbgoldbaltlem1  47767  sbgoldbm  47772  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbndlem4  47796  bgoldbtbnd  47797  grimedg  47923  cycl3grtri  47935  grlimgrtri  47991  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  lidldomn1  48219  2zrngamgm  48233  rngccatidALTV  48260  ringccatidALTV  48294  scmsuppss  48359  ply1mulgsumlem1  48375  lincsumcl  48420  ellcoellss  48424  lindslinindsimp1  48446  lindslinindimp2lem1  48447  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  itschlc0xyqsol1  48755