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  1114  3imp21  1116  meredith  1649  preqsnd  4755  3elpr2eq  4804  propeqop  5375  po2ne  5469  predpo  6158  funopg  6392  eldmrexrnb  6889  fvn0fvelrn  6956  peano5  7649  peano5OLD  7650  f1o2ndf1  7869  suppimacnv  7894  omordi  8272  omeulem1  8288  brecop  8470  isinf  8867  fiint  8926  carduni  9562  dfac5  9707  dfac2b  9709  cofsmo  9848  cfcoflem  9851  domtriomlem  10021  axdc3lem2  10030  nqereu  10508  squeeze0  11700  zmax  12506  elpq  12536  xnn0lenn0nn0  12800  xrsupsslem  12862  xrinfmsslem  12863  supxrunb1  12874  supxrunb2  12875  difreicc  13037  elfz0ubfz0  13181  elfz0fzfz0  13182  fz0fzelfz0  13183  fz0fzdiffz0  13186  fzo1fzo0n0  13258  elfzodifsumelfzo  13273  ssfzo12  13300  ssfzo12bi  13302  elfznelfzo  13312  injresinjlem  13327  injresinj  13328  addmodlteq  13484  uzindi  13520  ssnn0fi  13523  suppssfz  13532  facwordi  13820  hasheqf1oi  13883  hashf1rn  13884  fundmge2nop0  14023  swrdswrdlem  14234  swrdswrd  14235  wrd2ind  14253  swrdccatin1  14255  pfxccatin12lem2  14261  swrdccat  14265  reuccatpfxs1lem  14276  repsdf2  14308  cshwidx0  14336  cshweqrep  14351  2cshwcshw  14355  cshwcsh2id  14358  swrdco  14367  wwlktovfo  14490  sqrt2irr  15773  oddnn02np1  15872  oddge22np1  15873  evennn02n  15874  evennn2n  15875  dfgcd2  16069  lcmf  16153  lcmfunsnlem2lem2  16159  initoeu2lem1  17474  symgfix2  18762  gsmsymgreqlem2  18777  psgnunilem4  18843  lmodfopnelem1  19889  01eq0ring  20264  cply1mul  21169  gsummoncoe1  21179  mamufacex  21242  matecl  21276  gsummatr01  21510  mp2pm2mplem4  21660  chfacfscmul0  21709  chfacfpmmul0  21713  cayhamlem1  21717  fbunfip  22720  tngngp3  23508  zabsle1  26131  gausslemma2dlem1a  26200  2lgsoddprm  26251  2sqreunnltblem  26286  umgrnloopv  27151  upgredg2vtx  27186  usgruspgrb  27226  usgrnloopvALT  27243  usgredg2vlem2  27268  edg0usgr  27295  nbuhgr  27385  nbumgr  27389  nbuhgr2vtx1edgblem  27393  cusgredg  27466  cusgrsize2inds  27495  sizusglecusg  27505  umgr2v2enb1  27568  rusgr1vtx  27630  uspgr2wlkeq  27687  wlkreslem  27711  spthonepeq  27793  usgr2trlspth  27802  clwlkl1loop  27824  lfgrn1cycl  27843  uspgrn2crct  27846  crctcshwlkn0lem3  27850  crctcshwlkn0lem5  27852  wwlksnextbi  27932  wwlksnredwwlkn0  27934  wwlksnextinj  27937  wspthsnonn0vne  27955  umgr2adedgspth  27986  umgr2wlk  27987  usgr2wspthons3  28002  clwlkclwwlklem2a1  28029  clwlkclwwlklem2fv2  28033  clwlkclwwlklem2a4  28034  clwlkclwwlklem2a  28035  clwlkclwwlklem2  28037  clwwisshclwws  28052  erclwwlktr  28059  clwwlkn1loopb  28080  clwwlknwwlksnb  28092  clwwlkext2edg  28093  erclwwlkntr  28108  clwwlknon1  28134  clwwlknonwwlknonb  28143  clwwlknonex2lem2  28145  upgr1wlkdlem1  28182  upgr3v3e3cycl  28217  uhgr3cyclex  28219  upgr4cycl4dv4e  28222  eucrctshift  28280  frgr3vlem1  28310  3cyclfrgrrn1  28322  3cyclfrgrrn  28323  4cycl2vnunb  28327  frgrnbnb  28330  frgrncvvdeqlem8  28343  frgrwopreglem5  28358  frgrwopreglem5ALT  28359  frgr2wwlk1  28366  2clwwlk2clwwlk  28387  numclwwlk1lem2fo  28395  frgrreg  28431  friendshipgt3  28435  shmodsi  29424  kbass6  30156  mdsymlem6  30443  mdsymlem7  30444  cdj3lem2a  30471  cdj3lem3a  30474  satfrel  32996  gonarlem  33023  satffunlem1lem1  33031  satffunlem2lem1  33033  satffun  33038  wl-spae  35366  grpomndo  35719  rngoueqz  35784  zerdivemp1x  35791  elpcliN  37593  relexpiidm  40930  relexpxpmin  40943  ntrk0kbimka  41267  eel12131  41947  tratrbVD  42095  2uasbanhVD  42145  funressnfv  44152  funbrafv  44265  otiunsndisjX  44386  ssfz12  44422  fzoopth  44435  iccpartgt  44495  iccelpart  44501  iccpartnel  44506  fargshiftf1  44509  sprsymrelfvlem  44558  sprsymrelf1lem  44559  prproropf1olem4  44574  sbcpr  44589  reupr  44590  poprelb  44592  reuopreuprim  44594  fmtno4prmfac  44640  lighneallem4b  44677  lighneal  44679  mogoldbblem  44788  gbegt5  44829  sbgoldbaltlem1  44847  sbgoldbm  44852  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  bgoldbtbndlem4  44876  bgoldbtbnd  44877  isomuspgrlem2b  44897  isomuspgrlem2d  44899  lidldomn1  45095  2zrngamgm  45113  rngccatidALTV  45163  ringccatidALTV  45226  nzerooringczr  45246  scmsuppss  45324  ply1mulgsumlem1  45343  lincsumcl  45388  ellcoellss  45392  lindslinindsimp1  45414  lindslinindimp2lem1  45415  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582  itschlc0xyqsol1  45728