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  4823  3elpr2eq  4870  propeqop  5467  po2ne  5562  funopg  6550  eldmrexrnb  7064  fvn0fvelrnOLD  7135  peano5  7869  f1o2ndf1  8101  suppimacnv  8153  omordi  8530  omeulem1  8546  brecop  8783  isinf  9207  isinfOLD  9208  fiint  9277  fiintOLD  9278  carduni  9934  dfac5  10082  dfac2b  10084  cofsmo  10222  cfcoflem  10225  domtriomlem  10395  axdc3lem2  10404  nqereu  10882  squeeze0  12086  zmax  12904  elpq  12934  xnn0lenn0nn0  13205  xrsupsslem  13267  xrinfmsslem  13268  supxrunb1  13279  supxrunb2  13280  difreicc  13445  elfz0ubfz0  13593  elfz0fzfz0  13594  fz0fzelfz0  13595  fz0fzdiffz0  13598  fzo1fzo0n0  13676  elfzodifsumelfzo  13692  ssfzo12  13720  ssfzo12bi  13722  fzoopth  13723  elfznelfzo  13733  injresinjlem  13748  injresinj  13749  addmodlteq  13911  uzindi  13947  ssnn0fi  13950  suppssfz  13959  facwordi  14254  hasheqf1oi  14316  hashf1rn  14317  fundmge2nop0  14467  swrdswrdlem  14669  swrdswrd  14670  wrd2ind  14688  swrdccatin1  14690  pfxccatin12lem2  14696  swrdccat  14700  reuccatpfxs1lem  14711  repsdf2  14743  cshwidx0  14771  cshweqrep  14786  2cshwcshw  14791  cshwcsh2id  14794  swrdco  14803  wwlktovfo  14924  sqrt2irr  16217  oddnn02np1  16318  oddge22np1  16319  evennn02n  16320  evennn2n  16321  dfgcd2  16516  lcmf  16603  lcmfunsnlem2lem2  16609  initoeu2lem1  17976  symgfix2  19346  gsmsymgreqlem2  19361  psgnunilem4  19427  01eq0ringOLD  20440  lmodfopnelem1  20804  nzerooringczr  21390  cply1mul  22183  gsummoncoe1  22195  mamufacex  22283  matecl  22312  gsummatr01  22546  mp2pm2mplem4  22696  chfacfscmul0  22745  chfacfpmmul0  22749  cayhamlem1  22753  fbunfip  23756  tngngp3  24544  mpomulcn  24758  zabsle1  27207  gausslemma2dlem1a  27276  2lgsoddprm  27327  2sqreunnltblem  27362  umgrnloopv  29033  upgredg2vtx  29068  usgruspgrb  29110  usgrnloopvALT  29128  usgredg2vlem2  29153  edg0usgr  29180  nbuhgr  29270  nbumgr  29274  nbuhgr2vtx1edgblem  29278  cusgredg  29351  cusgrsize2inds  29381  sizusglecusg  29391  umgr2v2enb1  29454  rusgr1vtx  29516  uspgr2wlkeq  29574  wlkreslem  29597  spthonepeq  29682  usgr2trlspth  29691  clwlkl1loop  29713  lfgrn1cycl  29735  uspgrn2crct  29738  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  wwlksnextbi  29824  wwlksnredwwlkn0  29826  wwlksnextinj  29829  wspthsnonn0vne  29847  umgr2adedgspth  29878  umgr2wlk  29879  usgr2wspthons3  29894  clwlkclwwlklem2a1  29921  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwwisshclwws  29944  erclwwlktr  29951  clwwlkn1loopb  29972  clwwlknwwlksnb  29984  clwwlkext2edg  29985  erclwwlkntr  30000  clwwlknon1  30026  clwwlknonwwlknonb  30035  clwwlknonex2lem2  30037  upgr1wlkdlem1  30074  upgr3v3e3cycl  30109  uhgr3cyclex  30111  upgr4cycl4dv4e  30114  eucrctshift  30172  frgr3vlem1  30202  3cyclfrgrrn1  30214  3cyclfrgrrn  30215  4cycl2vnunb  30219  frgrnbnb  30222  frgrncvvdeqlem8  30235  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  frgr2wwlk1  30258  2clwwlk2clwwlk  30279  numclwwlk1lem2fo  30287  frgrreg  30323  friendshipgt3  30327  shmodsi  31318  kbass6  32050  mdsymlem6  32337  mdsymlem7  32338  cdj3lem2a  32365  cdj3lem3a  32368  satfrel  35354  gonarlem  35381  satffunlem1lem1  35389  satffunlem2lem1  35391  satffun  35396  wl-spae  37509  grpomndo  37869  rngoueqz  37934  zerdivemp1x  37941  elpcliN  39887  dflim5  43318  relexpiidm  43693  relexpxpmin  43706  ntrk0kbimka  44028  eel12131  44702  tratrbVD  44850  2uasbanhVD  44900  funressnfv  47044  funbrafv  47159  otiunsndisjX  47280  ssfz12  47315  iccpartgt  47428  iccelpart  47434  iccpartnel  47439  fargshiftf1  47442  sprsymrelfvlem  47491  sprsymrelf1lem  47492  prproropf1olem4  47507  sbcpr  47522  reupr  47523  poprelb  47525  reuopreuprim  47527  fmtno4prmfac  47573  lighneallem4b  47610  lighneal  47612  mogoldbblem  47721  gbegt5  47762  sbgoldbaltlem1  47780  sbgoldbm  47785  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  grimedg  47935  cycl3grtri  47946  grlimgrtri  47995  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  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