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  2256  moexexlem  2627  ralrimdvva  3193  ceqsal1t  3463  ceqsalt  3464  spcimgft  3492  vtoclgft  3498  elabgtOLD  3616  sbciegftOLD  3767  reupick  4270  reusv3  5342  sbcop1  5436  propeqop  5455  pwssun  5516  wefrc  5618  ssrel  5732  ssrel2  5734  ssrelrel  5745  ssrelrn  5843  tz7.7  6343  ordtr2  6362  onmindif  6411  unizlim  6441  funssres  6536  f1ssf1  6806  fvmptt  6962  fveqdmss  7024  fvcofneq  7039  funsndifnop  7098  funfvima2  7179  isoini  7286  isopolem  7293  weniso  7302  f1ocnv2d  7613  limsssuc  7794  tfindsg  7805  limomss  7815  findsg  7841  funcnvuni  7876  f1oweALT  7918  funelss  7993  bropopvvv  8033  bropfvvvvlem  8034  bropfvvvv  8035  f1o2ndf1  8065  frxp  8069  soseq  8102  suppfnss  8132  onfununi  8274  tz7.49  8377  omordi  8494  omlimcl  8506  omass  8508  oeordsuc  8523  nnmordi  8560  nnmord  8561  omabs  8580  xpdom2  9003  infensuc  9086  findcard2  9092  findcard2d  9094  findcard3  9186  frfi  9188  fsuppres  9299  dffi2  9329  elfiun  9336  ordiso2  9423  ordtypelem7  9432  suc11reg  9531  inf3lem2  9541  noinfep  9572  cantnfle  9583  cantnflem1  9601  cantnf  9605  ttrclss  9632  trcl  9640  epfrs  9643  frr3g  9671  r1sdom  9689  updjud  9849  dfac8alem  9942  indcardi  9954  alephordi  9987  dfac12lem3  10059  pwsdompw  10116  cofsmo  10182  cfcoflem  10185  coftr  10186  isf32lem2  10267  isf32lem9  10274  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  zorn2lem4  10412  zorn2lem6  10414  zorn2lem7  10415  ttukeylem6  10427  uniimadom  10457  konigthlem  10482  fpwwe2lem7  10551  tskord  10694  tskcard  10695  grupr  10711  gruiin  10724  grudomon  10731  grur1a  10733  genpn0  10917  genpcd  10920  distrlem5pr  10941  psslinpr  10945  ltaddpr  10948  ltexprlem3  10952  ltexprlem6  10955  ltapr  10959  prlem936  10961  suplem1pr  10966  axpre-sup  11083  1re  11135  dedekindle  11301  lemul12a  12004  divgt0  12015  divge0  12016  lbreu  12097  sup2  12103  bndndx  12427  elnnz  12525  nzadd  12566  fzind  12618  fnn0ind  12619  uzwo  12852  lbzbi  12877  zmax  12886  zbtwnre  12887  irradd  12914  irrmul  12915  ledivge1le  13006  xrub  13255  supxrunb2  13263  infmremnf  13287  iccid  13334  uzsubsubfz  13491  fzrevral  13557  elfz0fzfz0  13578  fz0fzelfz0  13579  elfzmlbp  13584  elincfzoext  13669  ssfzoulel  13706  ssfzo12bi  13707  fzoopth  13708  elfzonelfzo  13715  elfznelfzo  13719  elfznelfzob  13720  injresinjlem  13736  fleqceilz  13804  modaddmodup  13887  uzindi  13935  suppssfz  13947  mptnn0fsuppr  13952  le2sq2  14088  sqlecan  14162  facdiv  14240  facwordi  14242  faclbnd  14243  hashimarni  14394  hash2prd  14428  hashle2pr  14430  pr2pwpr  14432  fundmge2nop0  14455  fi1uzind  14460  brfi1indALT  14463  swrdnd2  14609  swrdnnn0nd  14610  swrdnd0  14611  pfxnd0  14642  swrdswrdlem  14657  swrdswrd  14658  ccatopth2  14670  wrd2ind  14676  pfxccatin12lem2a  14680  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12lem3  14685  swrdccat  14688  swrdccat3blem  14692  reuccatpfxs1lem  14699  repswswrd  14737  cshwidxmod  14756  cshwidx0  14759  2cshwcshw  14778  cshwcsh2id  14781  cau3lem  15308  caubnd  15312  climrlim2  15500  rlimcn3  15543  mulcn2  15549  climcau  15624  climbdd  15625  caucvg  15632  modfsummod  15748  p1modz1  16219  dvdsle  16270  dvdsdivcl  16276  ltoddhalfle  16321  halfleoddlt  16322  ndvdssub  16369  gcdcllem1  16459  dvdslegcd  16464  bezoutlem4  16502  dfgcd2  16506  lcmf  16593  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem  16601  lcmfdvdsb  16603  lcmfun  16605  coprmdvds1  16612  divgcdcoprm0  16625  cncongr1  16627  cncongr2  16628  prmfac1  16681  pcqcl  16818  dvdsprmpweqle  16848  oddprmdvds  16865  prmpwdvds  16866  infpnlem1  16872  prmgaplem5  17017  prmgaplem6  17018  prmgaplem7  17019  cshwshashlem1  17057  cictr  17763  initoeu2lem1  17972  initoeu2  17974  clatleglb  18475  lidrididd  18629  mulgaddcom  19065  mulginvcom  19066  cycsubm  19168  cyccom  19169  gsmsymgreqlem2  19397  symggen  19436  psgnunilem4  19463  sylow2blem3  19588  frgpnabllem1  19839  imasabl  19842  dprddisj2  20007  lmodfopnelem1  20884  lssssr  20940  lss1d  20949  lspsncv0  21136  rnglidlmcl  21206  rngqiprngimfo  21291  nzerooringczr  21470  pzriprnglem5  21475  pzriprnglem8  21478  znrrg  21555  mplcoe5lem  22027  cply1mul  22271  coe1fzgsumdlem  22278  gsummoncoe1  22283  evl1gsumdlem  22331  mamufacex  22371  dmatelnd  22471  scmataddcl  22491  scmatsubcl  22492  scmatmulcl  22493  smatvscl  22499  mavmulsolcl  22526  mdetdiagid  22575  cramerlem3  22664  pmatcoe1fsupp  22676  cpmatacl  22691  cpmatmcllem  22693  mp2pm2mplem4  22784  chpscmat  22817  chfacfisf  22829  chfacfisfcpmat  22830  uniopn  22872  opnnei  23095  neindisj2  23098  restcls  23156  restntr  23157  tgcnp  23228  subbascn  23229  iscnp4  23238  lpcls  23339  cmpsublem  23374  cmpsub  23375  tgcmp  23376  cmpcld  23377  dfconn2  23394  1stcrest  23428  2ndcdisj  23431  1stccnp  23437  comppfsc  23507  kgencn2  23532  txlm  23623  kqreglem1  23716  filin  23829  isfil2  23831  ufilmax  23882  ufileu  23894  filufint  23895  cfinufil  23903  elfm2  23923  rnelfmlem  23927  rnelfm  23928  flimopn  23950  fbflim2  23952  flffbas  23970  fclsnei  23994  flimfnfcls  24003  fclscmp  24005  fcfnei  24010  cnpfcf  24016  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  alexsubALT  24026  ptcmplem4  24030  qustgplem  24096  tsmsres  24119  tsmsxp  24130  metss  24483  metcnp3  24515  ovoliunnul  25484  ovolicc2lem3  25496  dyadmax  25575  itg2le  25716  bddiblnc  25819  itgcn  25822  ellimc3  25856  lhop1  25991  dvfsumrlim  26008  fta1g  26145  dvply2g  26261  fta1  26285  aalioulem3  26311  aalioulem4  26312  ulmcaulem  26372  ulmcau  26373  logbgcd1irr  26771  xrlimcnp  26945  cxploglim  26955  jensen  26966  lgsqrmodndvds  27330  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem3  27345  lgsquad2lem2  27362  2lgslem1a1  27366  2sqlem6  27400  2sq2  27410  2sqnn  27416  2sqreultblem  27425  nosepdmlem  27661  nodenselem8  27669  eqcuts3  27810  madebdaylemlrcut  27905  addsprop  27982  addsuniflem  28007  negsprop  28041  mulsprop  28136  mulsuniflem  28155  precsex  28224  onsfi  28362  elnnzs  28407  elreno2  28501  brbtwn2  28988  ax5seglem5  29016  axcontlem4  29050  axcontlem10  29056  umgrnloopv  29189  umgrnloop  29191  upgredgpr  29225  numedglnl  29227  usgrausgrb  29252  usgrnloopvALT  29284  usgrnloopALT  29286  usgredg2vlem2  29309  ushgredgedg  29312  ushgredgedgloop  29314  upgrreslem  29387  umgrreslem  29388  nbgr0edglem  29439  nbusgrvtxm1  29462  uvtxnbgrvtx  29476  cusgredg  29507  cusgrres  29532  cusgrsize2inds  29537  cusgrfi  29542  fusgrregdegfi  29653  ewlkle  29689  uspgr2wlkeqi  29731  lfgrwlkprop  29769  lfgrwlknloop  29771  pthdivtx  29810  2pthnloop  29814  upgrwlkdvdelem  29819  upgrspthswlk  29821  usgr2wlkneq  29839  usgr2trlncl  29843  usgr2pthlem  29846  usgr2pth  29847  uspgrn2crct  29891  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  crctcshwlkn0  29904  wlkiswwlks1  29950  wlkiswwlks2  29958  wlkiswwlksupgr2  29960  wwlksnred  29975  wwlksnext  29976  wwlksnextbi  29977  wwlksnextwrd  29980  wwlksnextinj  29982  wwlksnextproplem2  29993  wwlksnextproplem3  29994  wspthsnonn0vne  30000  wspn0  30007  2pthon3v  30026  usgrwwlks2on  30041  umgrwwlks2on  30042  elwspths2on  30045  elwspths2onw  30046  wpthswwlks2on  30047  clwwlk1loop  30073  clwwlkccatlem  30074  umgrclwwlkge2  30076  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlklem3  30086  clwlkclwwlkf1lem3  30091  clwlkclwwlkfo  30094  clwwisshclwwslemlem  30098  erclwwlkeqlen  30104  erclwwlksym  30106  clwwlkf  30132  clwwlknscsh  30147  erclwwlknsym  30155  clwwlknonex2lem2  30193  clwwlknonex2  30194  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eucrctshift  30328  3vfriswmgr  30363  1to2vfriswmgr  30364  1to3vfriswmgr  30365  n4cyclfrgr  30376  4cyclusnfrgr  30377  frgrnbnb  30378  frgrncvvdeqlem8  30391  frgrwopreg  30408  frgr2wwlk1  30414  frgr2wwlkeqm  30416  2clwwlk2clwwlklem  30431  numclwwlk1lem2fo  30443  wlkl0  30452  numclwlk2lem2f  30462  frgrreggt1  30478  frgrreg  30479  frgrregord013  30480  frgrregord13  30481  frgrogt3nreg  30482  eulplig  30571  nmoub3i  30859  ipasslem5  30921  htthlem  31003  ocin  31382  spansneleq  31656  spansnss  31657  elspansn4  31659  h1datomi  31667  nmopub2tALT  31995  nmfnleub2  32012  hstel2  32305  cvnbtwn  32372  spansncv2  32379  dmdmd  32386  dmdbr3  32391  dmdbr4  32392  dmdbr5  32394  mdsl0  32396  mdexchi  32421  cvexchlem  32454  atcv1  32466  atomli  32468  atcvatlem  32471  atcvat2i  32473  chirredi  32480  mdsymlem3  32491  mdsymlem4  32492  sumdmdii  32501  sumdmdlem  32504  cdj1i  32519  ssrelf  32703  f1o3d  32714  fisshasheq  35313  umgr2cycllem  35338  cvxpconn  35440  satfv0  35556  satfsschain  35562  satfrel  35565  satfdm  35567  satfv0fun  35569  sat1el2xp  35577  gonarlem  35592  goalrlem  35594  satffunlem1lem1  35600  satffunlem2lem1  35602  satffunlem2lem2  35604  satffun  35607  mrsubccat  35716  msubvrs  35758  fundmpss  35965  dfon2lem6  35984  dfon2lem8  35986  dfon2lem9  35987  dfon2  35988  wzel  36020  colinearxfr  36273  btwnconn1lem11  36295  lineintmo  36355  in-ax8  36422  ss-ax8  36423  trer  36514  elicc3  36515  finminlem  36516  nn0prpwlem  36520  fnessref  36555  neibastop2  36559  fgmin  36568  tailfb  36575  ordcmp  36645  ee7.2aOLD  36659  dfttc4  36728  bj-ceqsalt0  37207  bj-ceqsalt1  37208  isbasisrelowllem1  37685  isbasisrelowllem2  37686  relowlpssretop  37694  fvineqsneu  37741  fvineqsneq  37742  wl-mo3t  37915  finixpnum  37940  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem26  37981  poimirlem27  37982  poimirlem29  37984  ftc1anc  38036  fdc  38080  heibor1lem  38144  ghomco  38226  rngoueqz  38275  unichnidl  38366  dmncan1  38411  ax12indn  39403  lshpdisj  39447  lub0N  39649  glb0N  39653  leat2  39754  hlrelat2  39863  cvrexchlem  39879  cvratlem  39881  atcvrj0  39888  cvrat2  39889  snatpsubN  40210  linepsubN  40212  pmaple  40221  pmapsub  40228  elpaddn0  40260  paddasslem5  40284  trlval2  40623  cdlemn11pre  41670  dihord2pre  41685  mapdordlem2  42097  sn-sup2  42950  fsuppind  43037  pell1qrgap  43320  dford3lem1  43472  hbtlem5  43574  onexlimgt  43689  onsucf1olem  43716  omcl2  43779  tfsconcat0b  43792  ntrneiiso  44536  sbiota1  44879  19.41rg  44995  ee223  45079  or2expropbilem1  47492  funressnfv  47503  fcoresf1  47529  2reuimp  47575  f1oresf1o2  47751  zm1nn  47762  nltle2tri  47773  el1fzopredsuc  47786  modlt0b  47829  mod2addne  47830  muldvdsfacgt  47846  muldvdsfacm1  47847  elsetpreimafvssdm  47858  imasetpreimafvbijlemf1  47876  iccpartlt  47896  iccpartgt  47899  iccelpart  47905  icceuelpart  47908  iccpartnel  47910  fargshiftfo  47914  fargshiftfva  47915  lswn0  47916  ich2exprop  47943  prsprel  47959  sprsymrelfolem2  47965  sprsymrelfo  47969  poprelb  47996  reuopreuprim  47998  goldbachthlem2  48021  odz2prm2pw  48038  fmtnoprmfac1  48040  fmtnofac2lem  48043  prmdvdsfmtnof1lem2  48060  2pwp1prm  48064  sfprmdvdsmersenne  48078  lighneallem3  48082  requad01  48109  requad2  48111  even3prm2  48207  fppr2odd  48219  fpprwpprb  48228  gbegt5  48249  sbgoldbwt  48265  sbgoldbalt  48269  sbgoldbm  48272  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgblthelfgott  48303  tgoldbach  48305  isubgredg  48354  grimuhgr  48375  grimcnv  48376  grimco  48377  isuspgrim0  48382  isuspgrimlem  48383  uhgrimisgrgriclem  48418  clnbgrgrimlem  48421  grimedg  48423  grtriprop  48429  cycl3grtri  48435  grimgrtri  48437  isubgr3stgrlem6  48459  uspgrlimlem3  48478  uspgrlimlem4  48479  grlimgrtrilem2  48490  grlicsym  48501  clnbgr3stgrgrlim  48507  clnbgr3stgrgrlic  48508  gpgedg2ov  48554  gpgedg2iv  48555  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  upgrwlkupwlk  48628  lmod0rng  48717  ztprmneprm  48835  ply1mulgsumlem1  48874  ply1mulgsumlem2  48875  lcoel0  48916  linindslinci  48936  lindslinindimp2lem4  48949  lindslinindsimp2lem5  48950  snlindsntor  48959  ldepspr  48961  lincresunit2  48966  fllog2  49056  dignn0ldlem  49090  dignn0flhalflem1  49103  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  itcovalt2  49165  resum2sqorgt0  49197  eenglngeehlnmlem2  49226  rrx2linest  49230  itscnhlc0xyqsol  49253  itsclc0  49259  setrec1lem2  50175  aacllem  50288