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  647  an31s  650  3imp31  1105  3imp21  1107  meredith  1623  preqsnd  4700  3elpr2eq  4748  propeqop  5293  po2ne  5382  predpo  6046  funopg  6264  eldmrexrnb  6728  fvn0fvelrn  6793  peano5  7466  f1o2ndf1  7676  suppimacnv  7697  omordi  8047  omeulem1  8063  brecop  8245  isinf  8582  fiint  8646  carduni  9261  dfac5  9405  dfac2b  9407  cofsmo  9542  cfcoflem  9545  domtriomlem  9715  axdc3lem2  9724  nqereu  10202  squeeze0  11396  zmax  12199  elpq  12229  xnn0lenn0nn0  12493  xrsupsslem  12555  xrinfmsslem  12556  supxrunb1  12567  supxrunb2  12568  difreicc  12725  elfz0ubfz0  12866  elfz0fzfz0  12867  fz0fzelfz0  12868  fz0fzdiffz0  12871  fzo1fzo0n0  12943  elfzodifsumelfzo  12958  ssfzo12  12985  ssfzo12bi  12987  elfznelfzo  12997  injresinjlem  13012  injresinj  13013  addmodlteq  13169  uzindi  13205  ssnn0fi  13208  suppssfz  13217  facwordi  13504  hasheqf1oi  13567  hashf1rn  13568  fundmge2nop0  13701  swrdswrdlem  13907  swrdswrd  13908  wrd2ind  13926  swrdccatin1  13928  pfxccatin12lem2  13934  swrdccat  13938  reuccatpfxs1lem  13949  repsdf2  13981  cshwidx0  14009  cshweqrep  14024  2cshwcshw  14028  cshwcsh2id  14031  swrdco  14040  wwlktovfo  14161  sqrt2irr  15440  oddnn02np1  15535  oddge22np1  15536  evennn02n  15537  evennn2n  15538  dfgcd2  15728  lcmf  15811  lcmfunsnlem2lem2  15817  initoeu2lem1  17108  symgfix2  18280  gsmsymgreqlem2  18295  psgnunilem4  18361  lmodfopnelem1  19365  01eq0ring  19739  cply1mul  20150  gsummoncoe1  20160  mamufacex  20687  matecl  20723  gsummatr01  20957  mp2pm2mplem4  21106  chfacfscmul0  21155  chfacfpmmul0  21159  cayhamlem1  21163  fbunfip  22166  tngngp3  22953  zabsle1  25559  gausslemma2dlem1a  25628  2lgsoddprm  25679  2sqreunnltblem  25714  umgrnloopv  26579  upgredg2vtx  26614  usgruspgrb  26654  usgrnloopvALT  26671  usgredg2vlem2  26696  edg0usgr  26723  nbuhgr  26813  nbumgr  26817  nbuhgr2vtx1edgblem  26821  cusgredg  26894  cusgrsize2inds  26923  sizusglecusg  26933  umgr2v2enb1  26996  rusgr1vtx  27058  uspgr2wlkeq  27115  wlkreslem  27139  wlkreslemOLD  27141  spthonepeq  27225  usgr2trlspth  27234  clwlkl1loop  27256  lfgrn1cycl  27275  uspgrn2crct  27278  crctcshwlkn0lem3  27282  crctcshwlkn0lem5  27284  wwlksnextbi  27364  wwlksnredwwlkn0  27366  wwlksnextinj  27369  wspthsnonn0vne  27388  umgr2adedgspth  27419  umgr2wlk  27420  usgr2wspthons3  27435  clwlkclwwlklem2a1  27462  clwlkclwwlklem2fv2  27466  clwlkclwwlklem2a4  27467  clwlkclwwlklem2a  27468  clwlkclwwlklem2  27470  clwwisshclwws  27485  erclwwlktr  27492  clwwlkn1loopb  27513  clwwlknwwlksnb  27526  clwwlkext2edg  27527  erclwwlkntr  27542  clwwlknon1  27568  clwwlknonwwlknonb  27577  clwwlknonex2lem2  27579  upgr1wlkdlem1  27616  upgr3v3e3cycl  27651  uhgr3cyclex  27653  upgr4cycl4dv4e  27656  eucrctshift  27715  frgr3vlem1  27749  3cyclfrgrrn1  27761  3cyclfrgrrn  27762  4cycl2vnunb  27766  frgrnbnb  27769  frgrncvvdeqlem8  27782  frgrwopreglem5  27797  frgrwopreglem5ALT  27798  frgr2wwlk1  27805  2clwwlk2clwwlk  27826  numclwwlk1lem2fo  27834  frgrreg  27870  friendshipgt3  27874  shmodsi  28862  kbass6  29594  mdsymlem6  29881  mdsymlem7  29882  cdj3lem2a  29909  cdj3lem3a  29912  satfrel  32229  gonarlem  32256  satffunlem1lem1  32264  satffunlem2lem1  32266  satffun  32271  bj-snmoore  34031  wl-spae  34320  grpomndo  34711  rngoueqz  34776  zerdivemp1x  34783  elpcliN  36586  relexpiidm  39560  relexpxpmin  39573  ntrk0kbimka  39900  eel12131  40612  tratrbVD  40760  2uasbanhVD  40810  funressnfv  42821  funbrafv  42900  otiunsndisjX  43021  ssfz12  43057  fzoopth  43070  iccpartgt  43096  iccelpart  43102  iccpartnel  43107  fargshiftf1  43110  sprsymrelfvlem  43161  sprsymrelf1lem  43162  prproropf1olem4  43177  sbcpr  43192  reupr  43193  poprelb  43195  reuopreuprim  43197  fmtno4prmfac  43243  lighneallem4b  43283  lighneal  43285  mogoldbblem  43394  gbegt5  43435  sbgoldbaltlem1  43453  sbgoldbm  43458  bgoldbtbndlem2  43480  bgoldbtbndlem3  43481  bgoldbtbndlem4  43482  bgoldbtbnd  43483  isomuspgrlem2b  43503  isomuspgrlem2d  43505  lidldomn1  43697  2zrngamgm  43715  rngccatidALTV  43765  ringccatidALTV  43828  nzerooringczr  43848  scmsuppss  43927  ply1mulgsumlem1  43947  lincsumcl  43993  ellcoellss  43997  lindslinindsimp1  44019  lindslinindimp2lem1  44020  nn0sumshdiglemA  44187  nn0sumshdiglemB  44188  itschlc0xyqsol1  44261