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  650  an31s  653  3imp31  1112  3imp21  1114  meredith  1639  preqsnd  4883  3elpr2eq  4930  propeqop  5526  po2ne  5624  funopg  6612  eldmrexrnb  7126  fvn0fvelrnOLD  7197  peano5  7932  peano5OLD  7933  f1o2ndf1  8163  suppimacnv  8215  omordi  8622  omeulem1  8638  brecop  8868  isinf  9323  isinfOLD  9324  fiint  9394  fiintOLD  9395  carduni  10050  dfac5  10198  dfac2b  10200  cofsmo  10338  cfcoflem  10341  domtriomlem  10511  axdc3lem2  10520  nqereu  10998  squeeze0  12198  zmax  13010  elpq  13040  xnn0lenn0nn0  13307  xrsupsslem  13369  xrinfmsslem  13370  supxrunb1  13381  supxrunb2  13382  difreicc  13544  elfz0ubfz0  13689  elfz0fzfz0  13690  fz0fzelfz0  13691  fz0fzdiffz0  13694  fzo1fzo0n0  13767  elfzodifsumelfzo  13782  ssfzo12  13809  ssfzo12bi  13811  fzoopth  13812  elfznelfzo  13822  injresinjlem  13837  injresinj  13838  addmodlteq  13997  uzindi  14033  ssnn0fi  14036  suppssfz  14045  facwordi  14338  hasheqf1oi  14400  hashf1rn  14401  fundmge2nop0  14551  swrdswrdlem  14752  swrdswrd  14753  wrd2ind  14771  swrdccatin1  14773  pfxccatin12lem2  14779  swrdccat  14783  reuccatpfxs1lem  14794  repsdf2  14826  cshwidx0  14854  cshweqrep  14869  2cshwcshw  14874  cshwcsh2id  14877  swrdco  14886  wwlktovfo  15007  sqrt2irr  16297  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  dfgcd2  16593  lcmf  16680  lcmfunsnlem2lem2  16686  initoeu2lem1  18081  symgfix2  19458  gsmsymgreqlem2  19473  psgnunilem4  19539  01eq0ringOLD  20557  lmodfopnelem1  20918  nzerooringczr  21514  cply1mul  22321  gsummoncoe1  22333  mamufacex  22421  matecl  22452  gsummatr01  22686  mp2pm2mplem4  22836  chfacfscmul0  22885  chfacfpmmul0  22889  cayhamlem1  22893  fbunfip  23898  tngngp3  24698  mpomulcn  24910  zabsle1  27358  gausslemma2dlem1a  27427  2lgsoddprm  27478  2sqreunnltblem  27513  umgrnloopv  29141  upgredg2vtx  29176  usgruspgrb  29218  usgrnloopvALT  29236  usgredg2vlem2  29261  edg0usgr  29288  nbuhgr  29378  nbumgr  29382  nbuhgr2vtx1edgblem  29386  cusgredg  29459  cusgrsize2inds  29489  sizusglecusg  29499  umgr2v2enb1  29562  rusgr1vtx  29624  uspgr2wlkeq  29682  wlkreslem  29705  spthonepeq  29788  usgr2trlspth  29797  clwlkl1loop  29819  lfgrn1cycl  29838  uspgrn2crct  29841  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  wwlksnextbi  29927  wwlksnredwwlkn0  29929  wwlksnextinj  29932  wspthsnonn0vne  29950  umgr2adedgspth  29981  umgr2wlk  29982  usgr2wspthons3  29997  clwlkclwwlklem2a1  30024  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwwisshclwws  30047  erclwwlktr  30054  clwwlkn1loopb  30075  clwwlknwwlksnb  30087  clwwlkext2edg  30088  erclwwlkntr  30103  clwwlknon1  30129  clwwlknonwwlknonb  30138  clwwlknonex2lem2  30140  upgr1wlkdlem1  30177  upgr3v3e3cycl  30212  uhgr3cyclex  30214  upgr4cycl4dv4e  30217  eucrctshift  30275  frgr3vlem1  30305  3cyclfrgrrn1  30317  3cyclfrgrrn  30318  4cycl2vnunb  30322  frgrnbnb  30325  frgrncvvdeqlem8  30338  frgrwopreglem5  30353  frgrwopreglem5ALT  30354  frgr2wwlk1  30361  2clwwlk2clwwlk  30382  numclwwlk1lem2fo  30390  frgrreg  30426  friendshipgt3  30430  shmodsi  31421  kbass6  32153  mdsymlem6  32440  mdsymlem7  32441  cdj3lem2a  32468  cdj3lem3a  32471  satfrel  35335  gonarlem  35362  satffunlem1lem1  35370  satffunlem2lem1  35372  satffun  35377  wl-spae  37475  grpomndo  37835  rngoueqz  37900  zerdivemp1x  37907  elpcliN  39850  dflim5  43291  relexpiidm  43666  relexpxpmin  43679  ntrk0kbimka  44001  eel12131  44684  tratrbVD  44832  2uasbanhVD  44882  funressnfv  46958  funbrafv  47073  otiunsndisjX  47194  ssfz12  47229  iccpartgt  47301  iccelpart  47307  iccpartnel  47312  fargshiftf1  47315  sprsymrelfvlem  47364  sprsymrelf1lem  47365  prproropf1olem4  47380  sbcpr  47395  reupr  47396  poprelb  47398  reuopreuprim  47400  fmtno4prmfac  47446  lighneallem4b  47483  lighneal  47485  mogoldbblem  47594  gbegt5  47635  sbgoldbaltlem1  47653  sbgoldbm  47658  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  grimedg  47787  grlimgrtri  47820  lidldomn1  47954  2zrngamgm  47968  rngccatidALTV  47995  ringccatidALTV  48029  scmsuppss  48097  ply1mulgsumlem1  48115  lincsumcl  48160  ellcoellss  48164  lindslinindsimp1  48186  lindslinindimp2lem1  48187  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  itschlc0xyqsol1  48500