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  411  expcomd  416  impancom  451  a2and  846  dedlem0b  1045  sbequ1  2248  moexexlem  2626  ralrimdvva  3211  ceqsal1t  3514  ceqsalt  3515  spcimgft  3546  vtoclgft  3552  elabgt  3672  sbciegftOLD  3826  reupick  4329  reusv3  5405  sbcop1  5493  propeqop  5512  pwssun  5575  wefrc  5679  ssrel  5792  ssrelOLD  5793  ssrel2  5795  ssrelrel  5806  ssrelrn  5905  tz7.7  6410  ordtr2  6428  onmindif  6476  unizlim  6507  funssres  6610  f1ssf1  6880  fvmptt  7036  fveqdmss  7098  fvcofneq  7113  funsndifnop  7171  funfvima2  7251  isoini  7358  isopolem  7365  weniso  7374  f1ocnv2d  7686  limsssuc  7871  tfindsg  7882  limomss  7892  findsg  7919  funcnvuni  7954  f1oweALT  7997  funelss  8072  bropopvvv  8115  bropfvvvvlem  8116  bropfvvvv  8117  f1o2ndf1  8147  frxp  8151  soseq  8184  suppfnss  8214  wfrlem12OLD  8360  onfununi  8381  tz7.49  8485  omordi  8604  omlimcl  8616  omass  8618  oeordsuc  8632  nnmordi  8669  nnmord  8670  omabs  8689  xpdom2  9107  infensuc  9195  findcard2  9204  findcard2d  9206  findcard3  9318  findcard3OLD  9319  frfi  9321  xpfiOLD  9359  fsuppres  9433  dffi2  9463  elfiun  9470  ordiso2  9555  ordtypelem7  9564  suc11reg  9659  inf3lem2  9669  noinfep  9700  cantnfle  9711  cantnflem1  9729  cantnf  9733  ttrclss  9760  trcl  9768  epfrs  9771  frr3g  9796  r1sdom  9814  updjud  9974  pr2neOLD  10045  dfac8alem  10069  indcardi  10081  alephordi  10114  dfac12lem3  10186  pwsdompw  10243  cofsmo  10309  cfcoflem  10312  coftr  10313  isf32lem2  10394  isf32lem9  10401  axcc3  10478  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  zorn2lem4  10539  zorn2lem6  10541  zorn2lem7  10542  ttukeylem6  10554  uniimadom  10584  konigthlem  10608  fpwwe2lem7  10677  tskord  10820  tskcard  10821  grupr  10837  gruiin  10850  grudomon  10857  grur1a  10859  genpn0  11043  genpcd  11046  distrlem5pr  11067  psslinpr  11071  ltaddpr  11074  ltexprlem3  11078  ltexprlem6  11081  ltapr  11085  prlem936  11087  suplem1pr  11092  axpre-sup  11209  1re  11261  dedekindle  11425  lemul12a  12125  divgt0  12136  divge0  12137  lbreu  12218  sup2  12224  bndndx  12525  elnnz  12623  nzadd  12665  fzind  12716  fnn0ind  12717  uzwo  12953  lbzbi  12978  zmax  12987  zbtwnre  12988  irradd  13015  irrmul  13016  ledivge1le  13106  xrub  13354  supxrunb2  13362  infmremnf  13385  iccid  13432  uzsubsubfz  13586  fzrevral  13652  elfz0fzfz0  13673  fz0fzelfz0  13674  elfzmlbp  13679  elincfzoext  13762  ssfzoulel  13799  ssfzo12bi  13800  fzoopth  13801  elfzonelfzo  13808  elfznelfzo  13811  elfznelfzob  13812  injresinjlem  13826  fleqceilz  13894  modaddmodup  13975  uzindi  14023  suppssfz  14035  mptnn0fsuppr  14040  le2sq2  14175  sqlecan  14248  facdiv  14326  facwordi  14328  faclbnd  14329  hashimarni  14480  hash2prd  14514  hashle2pr  14516  pr2pwpr  14518  fundmge2nop0  14541  fi1uzind  14546  brfi1indALT  14549  swrdnd2  14693  swrdnnn0nd  14694  swrdnd0  14695  pfxnd0  14726  swrdswrdlem  14742  swrdswrd  14743  ccatopth2  14755  wrd2ind  14761  pfxccatin12lem2a  14765  swrdccatin2  14767  pfxccatin12lem2  14769  pfxccatin12lem3  14770  swrdccat  14773  swrdccat3blem  14777  reuccatpfxs1lem  14784  repswswrd  14822  cshwidxmod  14841  cshwidx0  14844  2cshwcshw  14864  cshwcsh2id  14867  cau3lem  15393  caubnd  15397  climrlim2  15583  rlimcn3  15626  mulcn2  15632  climcau  15707  climbdd  15708  caucvg  15715  modfsummod  15830  p1modz1  16297  dvdsle  16347  dvdsdivcl  16353  ltoddhalfle  16398  halfleoddlt  16399  ndvdssub  16446  gcdcllem1  16536  dvdslegcd  16541  bezoutlem4  16579  dfgcd2  16583  lcmf  16670  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem  16678  lcmfdvdsb  16680  lcmfun  16682  coprmdvds1  16689  divgcdcoprm0  16702  cncongr1  16704  cncongr2  16705  prmfac1  16757  pcqcl  16894  dvdsprmpweqle  16924  oddprmdvds  16941  prmpwdvds  16942  infpnlem1  16948  prmgaplem5  17093  prmgaplem6  17094  prmgaplem7  17095  cshwshashlem1  17133  cictr  17849  initoeu2lem1  18059  initoeu2  18061  clatleglb  18563  lidrididd  18683  mulgaddcom  19116  mulginvcom  19117  cycsubm  19220  cyccom  19221  gsmsymgreqlem2  19449  symggen  19488  psgnunilem4  19515  sylow2blem3  19640  frgpnabllem1  19891  imasabl  19894  dprddisj2  20059  lmodfopnelem1  20896  lssssr  20952  lss1d  20961  lspsncv0  21148  rnglidlmcl  21226  rngqiprngimfo  21311  nzerooringczr  21491  pzriprnglem5  21496  pzriprnglem8  21499  znrrg  21584  mplcoe5lem  22057  cply1mul  22300  coe1fzgsumdlem  22307  gsummoncoe1  22312  evl1gsumdlem  22360  mamufacex  22400  dmatelnd  22502  scmataddcl  22522  scmatsubcl  22523  scmatmulcl  22524  smatvscl  22530  mavmulsolcl  22557  mdetdiagid  22606  cramerlem3  22695  pmatcoe1fsupp  22707  cpmatacl  22722  cpmatmcllem  22724  mp2pm2mplem4  22815  chpscmat  22848  chfacfisf  22860  chfacfisfcpmat  22861  uniopn  22903  opnnei  23128  neindisj2  23131  restcls  23189  restntr  23190  tgcnp  23261  subbascn  23262  iscnp4  23271  lpcls  23372  cmpsublem  23407  cmpsub  23408  tgcmp  23409  cmpcld  23410  dfconn2  23427  1stcrest  23461  2ndcdisj  23464  1stccnp  23470  comppfsc  23540  kgencn2  23565  txlm  23656  kqreglem1  23749  filin  23862  isfil2  23864  ufilmax  23915  ufileu  23927  filufint  23928  cfinufil  23936  elfm2  23956  rnelfmlem  23960  rnelfm  23961  flimopn  23983  fbflim2  23985  flffbas  24003  fclsnei  24027  flimfnfcls  24036  fclscmp  24038  fcfnei  24043  cnpfcf  24049  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  ptcmplem4  24063  qustgplem  24129  tsmsres  24152  tsmsxp  24163  metss  24521  metcnp3  24553  ovoliunnul  25542  ovolicc2lem3  25554  dyadmax  25633  itg2le  25774  bddiblnc  25877  itgcn  25880  ellimc3  25914  lhop1  26053  dvfsumrlim  26072  fta1g  26209  dvply2g  26326  fta1  26350  aalioulem3  26376  aalioulem4  26377  ulmcaulem  26437  ulmcau  26438  logbgcd1irr  26837  xrlimcnp  27011  cxploglim  27021  jensen  27032  lgsqrmodndvds  27397  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem3  27412  lgsquad2lem2  27429  2lgslem1a1  27433  2sqlem6  27467  2sq2  27477  2sqnn  27483  2sqreultblem  27492  nosepdmlem  27728  nodenselem8  27736  madebdaylemlrcut  27937  addsprop  28009  addsuniflem  28034  negsprop  28067  mulsprop  28156  mulsuniflem  28175  precsex  28242  elnnzs  28387  brbtwn2  28920  ax5seglem5  28948  axcontlem4  28982  axcontlem10  28988  umgrnloopv  29123  umgrnloop  29125  upgredgpr  29159  numedglnl  29161  usgrausgrb  29186  usgrnloopvALT  29218  usgrnloopALT  29220  usgredg2vlem2  29243  ushgredgedg  29246  ushgredgedgloop  29248  upgrreslem  29321  umgrreslem  29322  nbgr0edglem  29373  nbusgrvtxm1  29396  uvtxnbgrvtx  29410  cusgredg  29441  cusgrres  29466  cusgrsize2inds  29471  cusgrfi  29476  fusgrregdegfi  29587  ewlkle  29623  uspgr2wlkeqi  29666  lfgrwlkprop  29705  lfgrwlknloop  29707  pthdivtx  29747  2pthnloop  29751  upgrwlkdvdelem  29756  upgrspthswlk  29758  usgr2wlkneq  29776  usgr2trlncl  29780  usgr2pthlem  29783  usgr2pth  29784  uspgrn2crct  29828  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0  29841  wlkiswwlks1  29887  wlkiswwlks2  29895  wlkiswwlksupgr2  29897  wwlksnred  29912  wwlksnext  29913  wwlksnextbi  29914  wwlksnextwrd  29917  wwlksnextinj  29919  wwlksnextproplem2  29930  wwlksnextproplem3  29931  wspthsnonn0vne  29937  wspn0  29944  2pthon3v  29963  umgrwwlks2on  29977  elwspths2on  29980  wpthswwlks2on  29981  clwwlk1loop  30007  clwwlkccatlem  30008  umgrclwwlkge2  30010  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem3  30020  clwlkclwwlkf1lem3  30025  clwlkclwwlkfo  30028  clwwisshclwwslemlem  30032  erclwwlkeqlen  30038  erclwwlksym  30040  clwwlkf  30066  clwwlknscsh  30081  erclwwlknsym  30089  clwwlknonex2lem2  30127  clwwlknonex2  30128  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eucrctshift  30262  3vfriswmgr  30297  1to2vfriswmgr  30298  1to3vfriswmgr  30299  n4cyclfrgr  30310  4cyclusnfrgr  30311  frgrnbnb  30312  frgrncvvdeqlem8  30325  frgrwopreg  30342  frgr2wwlk1  30348  frgr2wwlkeqm  30350  2clwwlk2clwwlklem  30365  numclwwlk1lem2fo  30377  wlkl0  30386  numclwlk2lem2f  30396  frgrreggt1  30412  frgrreg  30413  frgrregord013  30414  frgrregord13  30415  frgrogt3nreg  30416  eulplig  30504  nmoub3i  30792  ipasslem5  30854  htthlem  30936  ocin  31315  spansneleq  31589  spansnss  31590  elspansn4  31592  h1datomi  31600  nmopub2tALT  31928  nmfnleub2  31945  hstel2  32238  cvnbtwn  32305  spansncv2  32312  dmdmd  32319  dmdbr3  32324  dmdbr4  32325  dmdbr5  32327  mdsl0  32329  mdexchi  32354  cvexchlem  32387  atcv1  32399  atomli  32401  atcvatlem  32404  atcvat2i  32406  chirredi  32413  mdsymlem3  32424  mdsymlem4  32425  sumdmdii  32434  sumdmdlem  32437  cdj1i  32452  ssrelf  32627  f1o3d  32637  fisshasheq  35120  umgr2cycllem  35145  cvxpconn  35247  satfv0  35363  satfsschain  35369  satfrel  35372  satfdm  35374  satfv0fun  35376  sat1el2xp  35384  gonarlem  35399  goalrlem  35401  satffunlem1lem1  35407  satffunlem2lem1  35409  satffunlem2lem2  35411  satffun  35414  mrsubccat  35523  msubvrs  35565  fundmpss  35767  dfon2lem6  35789  dfon2lem8  35791  dfon2lem9  35792  dfon2  35793  wzel  35825  colinearxfr  36076  btwnconn1lem11  36098  lineintmo  36158  in-ax8  36225  ss-ax8  36226  trer  36317  elicc3  36318  finminlem  36319  nn0prpwlem  36323  fnessref  36358  neibastop2  36362  fgmin  36371  tailfb  36378  ordcmp  36448  ee7.2aOLD  36462  bj-cbvalimt  36640  bj-ceqsalt0  36885  bj-ceqsalt1  36886  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlpssretop  37365  fvineqsneu  37412  fvineqsneq  37413  wl-mo3t  37577  finixpnum  37612  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  ftc1anc  37708  fdc  37752  heibor1lem  37816  ghomco  37898  rngoueqz  37947  unichnidl  38038  dmncan1  38083  ax12indn  38944  lshpdisj  38988  lub0N  39190  glb0N  39194  leat2  39295  hlrelat2  39405  cvrexchlem  39421  cvratlem  39423  atcvrj0  39430  cvrat2  39431  snatpsubN  39752  linepsubN  39754  pmaple  39763  pmapsub  39770  elpaddn0  39802  paddasslem5  39826  trlval2  40165  cdlemn11pre  41212  dihord2pre  41227  mapdordlem2  41639  sn-sup2  42501  fsuppind  42600  pell1qrgap  42885  dford3lem1  43038  hbtlem5  43140  onexlimgt  43255  onsucf1olem  43283  omcl2  43346  tfsconcat0b  43359  ntrneiiso  44104  sbiota1  44453  19.41rg  44570  ee223  44654  or2expropbilem1  47044  funressnfv  47055  fcoresf1  47081  2reuimp  47127  f1oresf1o2  47303  zm1nn  47314  nltle2tri  47325  el1fzopredsuc  47337  elsetpreimafvssdm  47373  imasetpreimafvbijlemf1  47391  iccpartlt  47411  iccpartgt  47414  iccelpart  47420  icceuelpart  47423  iccpartnel  47425  fargshiftfo  47429  fargshiftfva  47430  lswn0  47431  ich2exprop  47458  prsprel  47474  sprsymrelfolem2  47480  sprsymrelfo  47484  poprelb  47511  reuopreuprim  47513  goldbachthlem2  47533  odz2prm2pw  47550  fmtnoprmfac1  47552  fmtnofac2lem  47555  prmdvdsfmtnof1lem2  47572  2pwp1prm  47576  sfprmdvdsmersenne  47590  lighneallem3  47594  requad01  47608  requad2  47610  even3prm2  47706  fppr2odd  47718  fpprwpprb  47727  gbegt5  47748  sbgoldbwt  47764  sbgoldbalt  47768  sbgoldbm  47771  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgblthelfgott  47802  tgoldbach  47804  isubgredg  47852  isuspgrim0  47872  isuspgrimlem  47874  grimuhgr  47878  grimcnv  47879  grimco  47880  uhgrimisgrgriclem  47898  clnbgrgrimlem  47901  grimedg  47903  grtriprop  47908  cycl3grtri  47914  grimgrtri  47916  isubgr3stgrlem6  47938  uspgrlimlem3  47957  uspgrlimlem4  47958  grlimgrtrilem2  47962  grlicsym  47973  clnbgr3stgrgrlic  47979  upgrwlkupwlk  48056  lmod0rng  48145  ztprmneprm  48263  ply1mulgsumlem1  48303  ply1mulgsumlem2  48304  lcoel0  48345  linindslinci  48365  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  snlindsntor  48388  ldepspr  48390  lincresunit2  48395  fllog2  48489  dignn0ldlem  48523  dignn0flhalflem1  48536  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  itcovalt2  48598  resum2sqorgt0  48630  eenglngeehlnmlem2  48659  rrx2linest  48663  itscnhlc0xyqsol  48686  itsclc0  48692  setrec1lem2  49207  aacllem  49320