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 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

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  96  an13s  663  an31s  666  3imp31  1129  3imp21  1131  meredith  1671  preqsnd  4825  3elpr2eq  4872  propeqop  5492  po2ne  5587  funopg  6572  eldmrexrnb  7089  peano5  7891  f1o2ndf1  8118  suppimacnv  8171  omordi  8552  omeulem1  8568  brecop  8809  isinf  9226  fiint  9287  carduni  9968  dfac5  10113  dfac2b  10115  cofsmo  10254  cfcoflem  10257  domtriomlem  10427  axdc3lem2  10436  nqereu  10915  squeeze0  12119  zmax  12970  elpq  13000  xnn0lenn0nn0  13272  xrsupsslem  13334  xrinfmsslem  13335  supxrunb1  13346  supxrunb2  13347  difreicc  13512  elfz0ubfz0  13662  elfz0fzfz0  13663  fz0fzelfz0  13664  fz0fzdiffz0  13667  fzo1fzo0n0  13746  elfzodifsumelfzo  13762  ssfzo12  13790  ssfzo12bi  13792  fzoopth  13793  elfznelfzo  13804  injresinjlem  13821  injresinj  13822  addmodlteq  13984  uzindi  14020  ssnn0fi  14023  suppssfz  14032  facwordi  14327  hasheqf1oi  14389  hashf1rn  14390  fundmge2nop0  14541  swrdswrdlem  14743  swrdswrd  14744  wrd2ind  14762  swrdccatin1  14764  pfxccatin12lem2  14770  swrdccat  14774  reuccatpfxs1lem  14785  repsdf2  14817  cshwidx0  14845  cshweqrep  14860  2cshwcshw  14864  cshwcsh2id  14867  swrdco  14876  wwlktovfo  14997  sqrt2irr  16306  oddnn02np1  16407  oddge22np1  16408  evennn02n  16409  evennn2n  16410  dfgcd2  16605  lcmf  16692  lcmfunsnlem2lem2  16698  initoeu2lem1  18072  symgfix2  19487  gsmsymgreqlem2  19502  psgnunilem4  19568  01eq0ringOLD  20616  lmodfopnelem1  21000  nzerooringczr  21611  cply1mul  22437  gsummoncoe1  22449  mamufacex  22534  matecl  22563  gsummatr01  22797  mp2pm2mplem4  22947  chfacfscmul0  22996  chfacfpmmul0  23000  cayhamlem1  23004  fbunfip  24007  tngngp3  24794  mpomulcn  25007  zabsle1  27438  gausslemma2dlem1a  27507  2lgsoddprm  27558  2sqreunnltblem  27593  umgrnloopv  29434  upgredg2vtx  29469  usgruspgrb  29511  usgrnloopvALT  29529  usgredg2vlem2  29554  edg0usgr  29581  nbuhgr  29671  nbumgr  29675  nbuhgr2vtx1edgblem  29679  cusgredg  29752  cusgrsize2inds  29781  sizusglecusg  29791  umgr2v2enb1  29854  rusgr1vtx  29916  uspgr2wlkeq  29973  wlkreslem  29995  spthonepeq  30079  usgr2trlspth  30088  clwlkl1loop  30110  lfgrn1cycl  30132  uspgrn2crct  30135  crctcshwlkn0lem3  30139  crctcshwlkn0lem5  30141  wwlksnextbi  30221  wwlksnredwwlkn0  30223  wwlksnextinj  30226  wspthsnonn0vne  30244  umgr2adedgspth  30275  umgr2wlk  30276  usgr2wspthons3  30294  clwlkclwwlklem2a1  30321  clwlkclwwlklem2fv2  30325  clwlkclwwlklem2a4  30326  clwlkclwwlklem2a  30327  clwlkclwwlklem2  30329  clwwisshclwws  30344  erclwwlktr  30351  clwwlkn1loopb  30372  clwwlknwwlksnb  30384  clwwlkext2edg  30385  erclwwlkntr  30400  clwwlknon1  30426  clwwlknonwwlknonb  30435  clwwlknonex2lem2  30437  upgr1wlkdlem1  30474  upgr3v3e3cycl  30509  uhgr3cyclex  30511  upgr4cycl4dv4e  30514  eucrctshift  30572  frgr3vlem1  30602  3cyclfrgrrn1  30614  3cyclfrgrrn  30615  4cycl2vnunb  30619  frgrnbnb  30622  frgrncvvdeqlem8  30635  frgrwopreglem5  30650  frgrwopreglem5ALT  30651  frgr2wwlk1  30658  2clwwlk2clwwlk  30679  numclwwlk1lem2fo  30687  frgrreg  30723  friendshipgt3  30727  shmodsi  31719  kbass6  32451  mdsymlem6  32738  mdsymlem7  32739  cdj3lem2a  32766  cdj3lem3a  32769  satfrel  35837  gonarlem  35864  satffunlem1lem1  35872  satffunlem2lem1  35874  satffun  35879  wl-spae  38154  grpomndo  38504  rngoueqz  38569  zerdivemp1x  38576  elpcliN  40645  dflim5  44036  relexpiidm  44410  relexpxpmin  44423  ntrk0kbimka  44745  eel12131  45401  tratrbVD  45549  2uasbanhVD  45599  funressnfv  47757  funbrafv  47872  otiunsndisjX  47993  ssfz12  48028  iccpartgt  48153  iccelpart  48159  iccpartnel  48164  fargshiftf1  48167  sprsymrelfvlem  48216  sprsymrelf1lem  48217  prproropf1olem4  48232  sbcpr  48247  reupr  48248  poprelb  48250  reuopreuprim  48252  fmtno4prmfac  48301  lighneallem4b  48338  lighneal  48340  nprmdvdsfacm1lem2  48350  mogoldbblem  48462  gbegt5  48503  sbgoldbaltlem1  48521  sbgoldbm  48526  bgoldbtbndlem2  48548  bgoldbtbndlem3  48549  bgoldbtbndlem4  48550  bgoldbtbnd  48551  grimedg  48677  cycl3grtri  48689  grlimgrtri  48745  pgnbgreunbgrlem2lem1  48856  pgnbgreunbgrlem2lem2  48857  pgnbgreunbgrlem2lem3  48858  lidldomn1  48973  2zrngamgm  48987  rngccatidALTV  49014  ringccatidALTV  49048  scmsuppss  49128  ply1mulgsumlem1  49143  lincsumcl  49188  ellcoellss  49192  lindslinindsimp1  49214  lindslinindimp2lem1  49215  nn0sumshdiglemA  49376  nn0sumshdiglemB  49377  itschlc0xyqsol1  49523