Theorem com23 86

Description: Commutation of antecedents. Swap 2nd and 3rd. Deduction associated with com12 32. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
com3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
com23	⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		pm2.27 42	. 2 ⊢ (𝜒 → ((𝜒 → 𝜃) → 𝜃))
3	1, 2	syl9 77	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:  com3r  87  com13  88  pm2.04  90  pm2.86d  108  impcomd  403  expcomd  409  impancom  444  a2and  831  dedlem0b  1025  sbequ1  2174  moexexvw  2656  2moswapv  2657  moexex  2664  ralrimdvva  3138  ceqsalt  3442  vtoclgft  3468  reu6  3625  sbciegft  3708  reupick  4169  reusv3  5153  sbcop1  5229  propeqop  5246  pwssun  5301  wefrc  5394  ssrel  5500  ssrel2  5502  ssrelrel  5512  ssrelrn  5606  predpo  5998  tz7.7  6049  ordtr2  6067  onmindif  6112  unizlim  6139  funssres  6225  f1ssf1  6469  fvmptt  6608  fveqdmss  6665  fvcofneq  6678  funsndifnop  6730  funfvima2  6813  isoini  6908  isopolem  6915  weniso  6924  f1ocnv2d  7210  limsssuc  7375  tfindsg  7385  limomss  7395  findsg  7418  funcnvuni  7445  f1oweALT  7478  bropopvvv  7586  bropfvvvvlem  7587  bropfvvvv  7588  f1o2ndf1  7616  frxp  7618  suppfnss  7651  wfrlem12  7763  onfununi  7775  tz7.49  7877  omordi  7985  omlimcl  7997  omass  7999  oeordsuc  8013  nnmordi  8050  nnmord  8051  omabs  8066  xpdom2  8400  infensuc  8483  findcard2  8545  findcard2d  8547  findcard3  8548  frfi  8550  xpfi  8576  fsuppres  8645  dffi2  8674  elfiun  8681  ordiso2  8766  ordtypelem7  8775  suc11reg  8868  inf3lem2  8878  noinfep  8909  cantnfle  8920  cantnflem1  8938  cantnf  8942  trcl  8956  epfrs  8959  r1sdom  8989  updjud  9149  pr2ne  9217  dfac8alem  9241  indcardi  9253  alephordi  9286  dfac12lem3  9357  pwsdompw  9416  cofsmo  9481  cfcoflem  9484  coftr  9485  isf32lem2  9566  isf32lem9  9573  axcc3  9650  domtriomlem  9654  axdc3lem2  9663  axdc3lem4  9665  zorn2lem4  9711  zorn2lem6  9713  zorn2lem7  9714  ttukeylem6  9726  uniimadom  9756  konigthlem  9780  fpwwe2lem8  9849  tskord  9992  tskcard  9993  grupr  10009  gruiin  10022  grudomon  10029  grur1a  10031  genpn0  10215  genpcd  10218  distrlem5pr  10239  psslinpr  10243  ltaddpr  10246  ltexprlem3  10250  ltexprlem6  10253  ltapr  10257  prlem936  10259  suplem1pr  10264  axpre-sup  10381  1re  10431  dedekindle  10596  lemul12a  11291  divgt0  11301  divge0  11302  lbreu  11384  sup2  11390  bndndx  11699  elnnz  11796  nzadd  11836  fzind  11886  fnn0ind  11887  uzwo  12118  lbzbi  12143  zmax  12152  zbtwnre  12153  irradd  12180  irrmul  12181  ledivge1le  12270  xrub  12514  supxrunb2  12522  infmremnf  12545  iccid  12592  uzsubsubfz  12738  fzrevral  12801  elfz0fzfz0  12821  fz0fzelfz0  12822  elfzmlbp  12827  elincfzoext  12903  ssfzoulel  12939  ssfzo12bi  12940  elfzonelfzo  12947  elfznelfzo  12950  elfznelfzob  12951  injresinjlem  12965  fleqceilz  13030  modaddmodup  13110  uzindi  13158  suppssfz  13170  mptnn0fsuppr  13175  le2sq2  13308  sqlecan  13379  facdiv  13455  facwordi  13457  faclbnd  13458  hashimarni  13605  hash2prd  13634  hashle2pr  13636  pr2pwpr  13638  fundmge2nop0  13651  fi1uzind  13656  brfi1indALT  13659  swrdnd2  13813  swrdnnn0nd  13814  swrdnd0  13815  pfxnd0  13860  swrdswrdlem  13876  swrdswrd  13877  ccatopth2  13899  wrd2ind  13907  wrd2indOLD  13908  reuccats1lemOLD  13910  swrdccatin12lem2a  13916  swrdccatin2  13919  pfxccatin12lem2  13921  swrdccatin12lem2OLD  13922  swrdccatin12lem3  13923  swrdccat  13928  swrdccatOLD  13929  swrdccat3blem  13934  reuccatpfxs1lem  13945  repswswrd  13993  cshwidxmod  14017  cshwidx0  14020  2cshwcshw  14039  cshwcsh2id  14042  cau3lem  14565  caubnd  14569  climrlim2  14755  rlimcn2  14798  mulcn2  14803  climcau  14878  climbdd  14879  caucvg  14886  modfsummod  14999  p1modz1  15464  dvdsle  15510  dvdsdivcl  15516  ltoddhalfle  15560  halfleoddlt  15561  ndvdssub  15610  gcdcllem1  15698  dvdslegcd  15703  bezoutlem4  15736  dfgcd2  15740  lcmf  15823  lcmfunsnlem1  15827  lcmfunsnlem2lem1  15828  lcmfunsnlem  15831  lcmfdvdsb  15833  lcmfun  15835  coprmdvds1  15842  divgcdcoprm0  15855  cncongr1  15857  cncongr2  15858  prmfac1  15909  pcqcl  16039  dvdsprmpweqle  16068  oddprmdvds  16085  prmpwdvds  16086  infpnlem1  16092  prmgaplem5  16237  prmgaplem6  16238  prmgaplem7  16239  cshwshashlem1  16275  cictr  16923  initoeu2lem1  17122  initoeu2  17124  clatleglb  17584  mulgaddcom  18025  mulginvcom  18026  gsmsymgreqlem2  18310  symggen  18349  psgnunilem4  18377  sylow2blem3  18498  frgpnabllem1  18739  dprddisj2  18901  f1rhm0to0ALT  19207  lmodfopnelem1  19382  lssssr  19437  lss1d  19447  lspsncv0  19630  mplcoe5lem  19951  cply1mul  20155  coe1fzgsumdlem  20162  gsummoncoe1  20165  evl1gsumdlem  20211  znrrg  20404  mamufacex  20692  dmatelnd  20799  scmataddcl  20819  scmatsubcl  20820  scmatmulcl  20821  smatvscl  20827  mavmulsolcl  20854  mdetdiagid  20903  cramerlem3  20992  pmatcoe1fsupp  21003  cpmatacl  21018  cpmatmcllem  21020  mp2pm2mplem4  21111  chpscmat  21144  chfacfisf  21156  chfacfisfcpmat  21157  uniopn  21199  opnnei  21422  neindisj2  21425  restcls  21483  restntr  21484  tgcnp  21555  subbascn  21556  iscnp4  21565  lpcls  21666  cmpsublem  21701  cmpsub  21702  tgcmp  21703  cmpcld  21704  dfconn2  21721  1stcrest  21755  2ndcdisj  21758  1stccnp  21764  comppfsc  21834  kgencn2  21859  txlm  21950  kqreglem1  22043  filin  22156  isfil2  22158  ufilmax  22209  ufileu  22221  filufint  22222  cfinufil  22230  elfm2  22250  rnelfmlem  22254  rnelfm  22255  flimopn  22277  fbflim2  22279  flffbas  22297  fclsnei  22321  flimfnfcls  22330  fclscmp  22332  fcfnei  22337  cnpfcf  22343  alexsubALTlem2  22350  alexsubALTlem3  22351  alexsubALTlem4  22352  alexsubALT  22353  ptcmplem4  22357  qustgplem  22422  tsmsres  22445  tsmsxp  22456  metss  22811  metcnp3  22843  ovoliunnul  23801  ovolicc2lem3  23813  dyadmax  23892  itg2le  24033  itgcn  24136  ellimc3  24170  lhop1  24304  dvfsumrlim  24321  fta1g  24454  fta1  24590  aalioulem3  24616  aalioulem4  24617  ulmcaulem  24675  ulmcau  24676  logbgcd1irr  25063  xrlimcnp  25238  cxploglim  25247  jensen  25258  lgsqrmodndvds  25621  gausslemma2dlem1a  25633  gausslemma2dlem2  25635  gausslemma2dlem3  25636  lgsquad2lem2  25653  2lgslem1a1  25657  2sqlem6  25691  2sq2  25701  2sqnn  25707  2sqreultblem  25716  brbtwn2  26384  ax5seglem5  26412  axcontlem4  26446  axcontlem10  26452  umgrnloopv  26584  umgrnloop  26586  upgredgpr  26620  numedglnl  26622  usgrausgrb  26647  usgrnloopvALT  26676  usgrnloopALT  26678  usgredg2vlem2  26701  ushgredgedg  26704  ushgredgedgloop  26706  upgrreslem  26779  umgrreslem  26780  nbgr0vtxlem  26830  nbusgrvtxm1  26854  uvtxnbgrvtx  26868  cusgredg  26899  cusgrres  26923  cusgrsize2inds  26928  cusgrfi  26933  fusgrregdegfi  27044  ewlkle  27080  uspgr2wlkeqi  27122  wlklenvclwlk  27129  lfgrwlkprop  27165  lfgrwlknloop  27167  pthdivtx  27208  2pthnloop  27210  upgrwlkdvdelem  27215  upgrspthswlk  27217  usgr2wlkneq  27235  usgr2trlncl  27239  usgr2pthlem  27242  usgr2pth  27243  uspgrn2crct  27284  crctcshwlkn0lem4  27289  crctcshwlkn0lem5  27290  crctcshwlkn0  27297  wlkiswwlks1  27343  wlkiswwlks2  27351  wlkiswwlksupgr2  27353  wwlksnred  27369  wwlksnredOLD  27370  wwlksnext  27371  wwlksnextbi  27372  wwlksnextbiOLD  27373  wwlksnextwrd  27378  wwlksnextinj  27380  wwlksnextwrdOLD  27383  wwlksnextinjOLD  27385  wwlksnextproplem2  27401  wwlksnextproplem2OLD  27402  wwlksnextproplem3  27403  wwlksnextproplem3OLD  27404  wspthsnonn0vne  27413  wspn0  27420  2pthon3v  27439  umgrwwlks2on  27453  elwspths2on  27456  wpthswwlks2on  27457  clwwlk1loop  27484  clwwlkccatlem  27485  umgrclwwlkge2  27487  clwlkclwwlklem2a4  27493  clwlkclwwlklem2a  27494  clwlkclwwlklem3  27497  clwlkclwwlkf1lem3  27505  clwlkclwwlkf1lem3OLD  27506  clwlkclwwlkfoOLD  27509  clwlkclwwlkfo  27513  clwwisshclwwslemlem  27518  erclwwlkeqlen  27524  erclwwlksym  27526  clwwlkfOLD  27554  clwwlkf  27559  clwwlknscsh  27576  erclwwlknsym  27584  clwwlknonex2lem2  27626  clwwlknonex2  27627  upgr3v3e3cycl  27699  upgr4cycl4dv4e  27704  eucrctshift  27763  3vfriswmgr  27802  1to2vfriswmgr  27803  1to3vfriswmgr  27804  n4cyclfrgr  27815  4cyclusnfrgr  27816  frgrnbnb  27817  frgrncvvdeqlem8  27830  frgrwopreg  27847  frgr2wwlk1  27853  frgr2wwlkeqm  27855  2clwwlk2clwwlklem  27873  numclwwlk1lem2fo  27890  numclwwlk1lem2foOLD  27895  wlkl0  27910  numclwlk2lem2f  27920  numclwlk2lem2fOLD  27923  frgrreggt1  27940  frgrreg  27941  frgrregord013  27942  frgrregord13  27943  frgrogt3nreg  27944  eulplig  28029  nmoub3i  28317  ipasslem5  28379  htthlem  28463  ocin  28844  spansneleq  29118  spansnss  29119  elspansn4  29121  h1datomi  29129  nmopub2tALT  29457  nmfnleub2  29474  hstel2  29767  cvnbtwn  29834  spansncv2  29841  dmdmd  29848  dmdbr3  29853  dmdbr4  29854  dmdbr5  29856  mdsl0  29858  mdexchi  29883  cvexchlem  29916  atcv1  29928  atomli  29930  atcvatlem  29933  atcvat2i  29935  chirredi  29942  mdsymlem3  29953  mdsymlem4  29954  sumdmdii  29963  sumdmdlem  29966  cdj1i  29981  ssrelf  30120  f1o3d  30126  cvxpconn  32034  mrsubccat  32225  msubvrs  32267  fundmpss  32469  dfon2lem6  32493  dfon2lem8  32495  dfon2lem9  32496  dfon2  32497  trpredrec  32538  soseq  32557  wzel  32572  frr3g  32582  nosepdmlem  32648  nodenselem8  32656  colinearxfr  32997  btwnconn1lem11  33019  lineintmo  33079  trer  33125  elicc3  33126  finminlem  33127  nn0prpwlem  33131  fnessref  33166  neibastop2  33170  fgmin  33179  tailfb  33186  ordcmp  33255  ee7.2aOLD  33269  bj-cbvalimt  33421  bj-ceqsalt0  33633  bj-ceqsalt1  33634  isbasisrelowllem1  34013  isbasisrelowllem2  34014  relowlpssretop  34022  fvineqsneu  34068  fvineqsneq  34069  wl-mo3t  34201  finixpnum  34266  matunitlindflem1  34277  matunitlindflem2  34278  poimirlem26  34307  poimirlem27  34308  poimirlem29  34310  bddiblnc  34351  ftc1anc  34364  fdc  34410  heibor1lem  34477  ghomco  34559  rngoueqz  34608  unichnidl  34699  dmncan1  34744  ax12indn  35472  lshpdisj  35516  lub0N  35718  glb0N  35722  leat2  35823  hlrelat2  35932  cvrexchlem  35948  cvratlem  35950  atcvrj0  35957  cvrat2  35958  snatpsubN  36279  linepsubN  36281  pmaple  36290  pmapsub  36297  elpaddn0  36329  paddasslem5  36353  trlval2  36692  cdlemn11pre  37739  dihord2pre  37754  mapdordlem2  38166  pell1qrgap  38812  dford3lem1  38964  hbtlem5  39069  ntrneiiso  39749  sbiota1  40127  19.41rg  40247  ee223  40331  or2expropbilem1  42618  funressnfv  42629  2reuimp  42666  f1oresf1o2  42842  zm1nn  42854  nltle2tri  42865  el1fzopredsuc  42877  fzoopth  42879  iccpartlt  42902  iccpartgt  42905  iccelpart  42911  icceuelpart  42914  iccpartnel  42916  fargshiftfo  42920  fargshiftfva  42921  lswn0  42922  ich2exprop  42941  prsprel  42957  sprsymrelfolem2  42963  sprsymrelfo  42967  poprelb  42994  reuopreuprim  42996  goldbachthlem2  43016  odz2prm2pw  43033  fmtnoprmfac1  43035  fmtnofac2lem  43038  prmdvdsfmtnof1lem2  43055  2pwp1prm  43059  sfprmdvdsmersenne  43076  lighneallem3  43080  requad01  43094  requad2  43096  even3prm2  43192  fppr2odd  43204  fpprwpprb  43213  gbegt5  43234  sbgoldbwt  43250  sbgoldbalt  43254  sbgoldbm  43257  bgoldbtbndlem2  43279  bgoldbtbndlem3  43280  bgoldbtbndlem4  43281  bgoldbtbnd  43282  tgblthelfgott  43288  tgoldbach  43290  isomuspgrlem2b  43302  isomuspgrlem2d  43304  isomuspgr  43307  isomgrsym  43309  upgrwlkupwlk  43323  lmod0rng  43443  nzerooringczr  43647  ztprmneprm  43699  ply1mulgsumlem1  43747  ply1mulgsumlem2  43748  lcoel0  43790  linindslinci  43810  lindslinindimp2lem4  43823  lindslinindsimp2lem5  43824  snlindsntor  43833  ldepspr  43835  lincresunit2  43840  fllog2  43936  dignn0ldlem  43970  dignn0flhalflem1  43983  nn0sumshdiglemA  43987  nn0sumshdiglemB  43988  resum2sqorgt0  44004  eenglngeehlnmlem2  44033  rrx2linest  44037  itscnhlc0xyqsol  44060  itsclc0  44066  setrec1lem2  44098  aacllem  44209