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  649  an31s  652  3imp31  1109  3imp21  1111  meredith  1635  preqsnd  4864  3elpr2eq  4911  propeqop  5512  po2ne  5609  funopg  6592  eldmrexrnb  7105  fvn0fvelrnOLD  7176  peano5  7904  peano5OLD  7905  f1o2ndf1  8135  suppimacnv  8187  omordi  8595  omeulem1  8611  brecop  8838  isinf  9297  isinfOLD  9298  fiint  9363  fiintOLD  9364  carduni  10020  dfac5  10167  dfac2b  10169  cofsmo  10308  cfcoflem  10311  domtriomlem  10481  axdc3lem2  10490  nqereu  10968  squeeze0  12164  zmax  12976  elpq  13006  xnn0lenn0nn0  13273  xrsupsslem  13335  xrinfmsslem  13336  supxrunb1  13347  supxrunb2  13348  difreicc  13510  elfz0ubfz0  13654  elfz0fzfz0  13655  fz0fzelfz0  13656  fz0fzdiffz0  13659  fzo1fzo0n0  13732  elfzodifsumelfzo  13747  ssfzo12  13774  ssfzo12bi  13776  fzoopth  13777  elfznelfzo  13787  injresinjlem  13802  injresinj  13803  addmodlteq  13961  uzindi  13997  ssnn0fi  14000  suppssfz  14009  facwordi  14301  hasheqf1oi  14363  hashf1rn  14364  fundmge2nop0  14506  swrdswrdlem  14707  swrdswrd  14708  wrd2ind  14726  swrdccatin1  14728  pfxccatin12lem2  14734  swrdccat  14738  reuccatpfxs1lem  14749  repsdf2  14781  cshwidx0  14809  cshweqrep  14824  2cshwcshw  14829  cshwcsh2id  14832  swrdco  14841  wwlktovfo  14962  sqrt2irr  16246  oddnn02np1  16345  oddge22np1  16346  evennn02n  16347  evennn2n  16348  dfgcd2  16542  lcmf  16629  lcmfunsnlem2lem2  16635  initoeu2lem1  18031  symgfix2  19409  gsmsymgreqlem2  19424  psgnunilem4  19490  01eq0ringOLD  20508  lmodfopnelem1  20821  nzerooringczr  21462  cply1mul  22279  gsummoncoe1  22291  mamufacex  22379  matecl  22410  gsummatr01  22644  mp2pm2mplem4  22794  chfacfscmul0  22843  chfacfpmmul0  22847  cayhamlem1  22851  fbunfip  23856  tngngp3  24656  mpomulcn  24868  zabsle1  27317  gausslemma2dlem1a  27386  2lgsoddprm  27437  2sqreunnltblem  27472  umgrnloopv  29034  upgredg2vtx  29069  usgruspgrb  29111  usgrnloopvALT  29129  usgredg2vlem2  29154  edg0usgr  29181  nbuhgr  29271  nbumgr  29275  nbuhgr2vtx1edgblem  29279  cusgredg  29352  cusgrsize2inds  29382  sizusglecusg  29392  umgr2v2enb1  29455  rusgr1vtx  29517  uspgr2wlkeq  29575  wlkreslem  29598  spthonepeq  29681  usgr2trlspth  29690  clwlkl1loop  29712  lfgrn1cycl  29731  uspgrn2crct  29734  crctcshwlkn0lem3  29738  crctcshwlkn0lem5  29740  wwlksnextbi  29820  wwlksnredwwlkn0  29822  wwlksnextinj  29825  wspthsnonn0vne  29843  umgr2adedgspth  29874  umgr2wlk  29875  usgr2wspthons3  29890  clwlkclwwlklem2a1  29917  clwlkclwwlklem2fv2  29921  clwlkclwwlklem2a4  29922  clwlkclwwlklem2a  29923  clwlkclwwlklem2  29925  clwwisshclwws  29940  erclwwlktr  29947  clwwlkn1loopb  29968  clwwlknwwlksnb  29980  clwwlkext2edg  29981  erclwwlkntr  29996  clwwlknon1  30022  clwwlknonwwlknonb  30031  clwwlknonex2lem2  30033  upgr1wlkdlem1  30070  upgr3v3e3cycl  30105  uhgr3cyclex  30107  upgr4cycl4dv4e  30110  eucrctshift  30168  frgr3vlem1  30198  3cyclfrgrrn1  30210  3cyclfrgrrn  30211  4cycl2vnunb  30215  frgrnbnb  30218  frgrncvvdeqlem8  30231  frgrwopreglem5  30246  frgrwopreglem5ALT  30247  frgr2wwlk1  30254  2clwwlk2clwwlk  30275  numclwwlk1lem2fo  30283  frgrreg  30319  friendshipgt3  30323  shmodsi  31314  kbass6  32046  mdsymlem6  32333  mdsymlem7  32334  cdj3lem2a  32361  cdj3lem3a  32364  satfrel  35147  gonarlem  35174  satffunlem1lem1  35182  satffunlem2lem1  35184  satffun  35189  wl-spae  37164  grpomndo  37524  rngoueqz  37589  zerdivemp1x  37596  elpcliN  39540  dflim5  42932  relexpiidm  43308  relexpxpmin  43321  ntrk0kbimka  43643  eel12131  44326  tratrbVD  44474  2uasbanhVD  44524  funressnfv  46595  funbrafv  46708  otiunsndisjX  46829  ssfz12  46864  iccpartgt  46936  iccelpart  46942  iccpartnel  46947  fargshiftf1  46950  sprsymrelfvlem  46999  sprsymrelf1lem  47000  prproropf1olem4  47015  sbcpr  47030  reupr  47031  poprelb  47033  reuopreuprim  47035  fmtno4prmfac  47081  lighneallem4b  47118  lighneal  47120  mogoldbblem  47229  gbegt5  47270  sbgoldbaltlem1  47288  sbgoldbm  47293  bgoldbtbndlem2  47315  bgoldbtbndlem3  47316  bgoldbtbndlem4  47317  bgoldbtbnd  47318  lidldomn1  47545  2zrngamgm  47559  rngccatidALTV  47586  ringccatidALTV  47620  scmsuppss  47688  ply1mulgsumlem1  47706  lincsumcl  47751  ellcoellss  47755  lindslinindsimp1  47777  lindslinindimp2lem1  47778  nn0sumshdiglemA  47944  nn0sumshdiglemB  47945  itschlc0xyqsol1  48091