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  2626  ralrimdvva  3192  ceqsal1t  3462  ceqsalt  3463  spcimgft  3491  vtoclgft  3497  elabgtOLD  3615  sbciegftOLD  3766  reupick  4269  reusv3  5347  sbcop1  5441  propeqop  5461  pwssun  5523  wefrc  5625  ssrel  5739  ssrel2  5741  ssrelrel  5752  ssrelrn  5849  tz7.7  6349  ordtr2  6368  onmindif  6417  unizlim  6447  funssres  6542  f1ssf1  6812  fvmptt  6968  fveqdmss  7030  fvcofneq  7045  funsndifnop  7105  funfvima2  7186  isoini  7293  isopolem  7300  weniso  7309  f1ocnv2d  7620  limsssuc  7801  tfindsg  7812  limomss  7822  findsg  7848  funcnvuni  7883  f1oweALT  7925  funelss  8000  bropopvvv  8040  bropfvvvvlem  8041  bropfvvvv  8042  f1o2ndf1  8072  frxp  8076  soseq  8109  suppfnss  8139  onfununi  8281  tz7.49  8384  omordi  8501  omlimcl  8513  omass  8515  oeordsuc  8530  nnmordi  8567  nnmord  8568  omabs  8587  xpdom2  9010  infensuc  9093  findcard2  9099  findcard2d  9101  findcard3  9193  frfi  9195  fsuppres  9306  dffi2  9336  elfiun  9343  ordiso2  9430  ordtypelem7  9439  suc11reg  9540  inf3lem2  9550  noinfep  9581  cantnfle  9592  cantnflem1  9610  cantnf  9614  ttrclss  9641  trcl  9649  epfrs  9652  frr3g  9680  r1sdom  9698  updjud  9858  dfac8alem  9951  indcardi  9963  alephordi  9996  dfac12lem3  10068  pwsdompw  10125  cofsmo  10191  cfcoflem  10194  coftr  10195  isf32lem2  10276  isf32lem9  10283  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  zorn2lem4  10421  zorn2lem6  10423  zorn2lem7  10424  ttukeylem6  10436  uniimadom  10466  konigthlem  10491  fpwwe2lem7  10560  tskord  10703  tskcard  10704  grupr  10720  gruiin  10733  grudomon  10740  grur1a  10742  genpn0  10926  genpcd  10929  distrlem5pr  10950  psslinpr  10954  ltaddpr  10957  ltexprlem3  10961  ltexprlem6  10964  ltapr  10968  prlem936  10970  suplem1pr  10975  axpre-sup  11092  1re  11144  dedekindle  11310  lemul12a  12013  divgt0  12024  divge0  12025  lbreu  12106  sup2  12112  bndndx  12436  elnnz  12534  nzadd  12575  fzind  12627  fnn0ind  12628  uzwo  12861  lbzbi  12886  zmax  12895  zbtwnre  12896  irradd  12923  irrmul  12924  ledivge1le  13015  xrub  13264  supxrunb2  13272  infmremnf  13296  iccid  13343  uzsubsubfz  13500  fzrevral  13566  elfz0fzfz0  13587  fz0fzelfz0  13588  elfzmlbp  13593  elincfzoext  13678  ssfzoulel  13715  ssfzo12bi  13716  fzoopth  13717  elfzonelfzo  13724  elfznelfzo  13728  elfznelfzob  13729  injresinjlem  13745  fleqceilz  13813  modaddmodup  13896  uzindi  13944  suppssfz  13956  mptnn0fsuppr  13961  le2sq2  14097  sqlecan  14171  facdiv  14249  facwordi  14251  faclbnd  14252  hashimarni  14403  hash2prd  14437  hashle2pr  14439  pr2pwpr  14441  fundmge2nop0  14464  fi1uzind  14469  brfi1indALT  14472  swrdnd2  14618  swrdnnn0nd  14619  swrdnd0  14620  pfxnd0  14651  swrdswrdlem  14666  swrdswrd  14667  ccatopth2  14679  wrd2ind  14685  pfxccatin12lem2a  14689  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12lem3  14694  swrdccat  14697  swrdccat3blem  14701  reuccatpfxs1lem  14708  repswswrd  14746  cshwidxmod  14765  cshwidx0  14768  2cshwcshw  14787  cshwcsh2id  14790  cau3lem  15317  caubnd  15321  climrlim2  15509  rlimcn3  15552  mulcn2  15558  climcau  15633  climbdd  15634  caucvg  15641  modfsummod  15757  p1modz1  16228  dvdsle  16279  dvdsdivcl  16285  ltoddhalfle  16330  halfleoddlt  16331  ndvdssub  16378  gcdcllem1  16468  dvdslegcd  16473  bezoutlem4  16511  dfgcd2  16515  lcmf  16602  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem  16610  lcmfdvdsb  16612  lcmfun  16614  coprmdvds1  16621  divgcdcoprm0  16634  cncongr1  16636  cncongr2  16637  prmfac1  16690  pcqcl  16827  dvdsprmpweqle  16857  oddprmdvds  16874  prmpwdvds  16875  infpnlem1  16881  prmgaplem5  17026  prmgaplem6  17027  prmgaplem7  17028  cshwshashlem1  17066  cictr  17772  initoeu2lem1  17981  initoeu2  17983  clatleglb  18484  lidrididd  18638  mulgaddcom  19074  mulginvcom  19075  cycsubm  19177  cyccom  19178  gsmsymgreqlem2  19406  symggen  19445  psgnunilem4  19472  sylow2blem3  19597  frgpnabllem1  19848  imasabl  19851  dprddisj2  20016  lmodfopnelem1  20893  lssssr  20949  lss1d  20958  lspsncv0  21144  rnglidlmcl  21214  rngqiprngimfo  21299  nzerooringczr  21460  pzriprnglem5  21465  pzriprnglem8  21468  znrrg  21545  mplcoe5lem  22017  cply1mul  22261  coe1fzgsumdlem  22268  gsummoncoe1  22273  evl1gsumdlem  22321  mamufacex  22361  dmatelnd  22461  scmataddcl  22481  scmatsubcl  22482  scmatmulcl  22483  smatvscl  22489  mavmulsolcl  22516  mdetdiagid  22565  cramerlem3  22654  pmatcoe1fsupp  22666  cpmatacl  22681  cpmatmcllem  22683  mp2pm2mplem4  22774  chpscmat  22807  chfacfisf  22819  chfacfisfcpmat  22820  uniopn  22862  opnnei  23085  neindisj2  23088  restcls  23146  restntr  23147  tgcnp  23218  subbascn  23219  iscnp4  23228  lpcls  23329  cmpsublem  23364  cmpsub  23365  tgcmp  23366  cmpcld  23367  dfconn2  23384  1stcrest  23418  2ndcdisj  23421  1stccnp  23427  comppfsc  23497  kgencn2  23522  txlm  23613  kqreglem1  23706  filin  23819  isfil2  23821  ufilmax  23872  ufileu  23884  filufint  23885  cfinufil  23893  elfm2  23913  rnelfmlem  23917  rnelfm  23918  flimopn  23940  fbflim2  23942  flffbas  23960  fclsnei  23984  flimfnfcls  23993  fclscmp  23995  fcfnei  24000  cnpfcf  24006  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  ptcmplem4  24020  qustgplem  24086  tsmsres  24109  tsmsxp  24120  metss  24473  metcnp3  24505  ovoliunnul  25474  ovolicc2lem3  25486  dyadmax  25565  itg2le  25706  bddiblnc  25809  itgcn  25812  ellimc3  25846  lhop1  25981  dvfsumrlim  25998  fta1g  26135  dvply2g  26251  fta1  26274  aalioulem3  26300  aalioulem4  26301  ulmcaulem  26359  ulmcau  26360  logbgcd1irr  26758  xrlimcnp  26932  cxploglim  26941  jensen  26952  lgsqrmodndvds  27316  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  lgsquad2lem2  27348  2lgslem1a1  27352  2sqlem6  27386  2sq2  27396  2sqnn  27402  2sqreultblem  27411  nosepdmlem  27647  nodenselem8  27655  eqcuts3  27796  madebdaylemlrcut  27891  addsprop  27968  addsuniflem  27993  negsprop  28027  mulsprop  28122  mulsuniflem  28141  precsex  28210  onsfi  28348  elnnzs  28393  elreno2  28487  brbtwn2  28974  ax5seglem5  29002  axcontlem4  29036  axcontlem10  29042  umgrnloopv  29175  umgrnloop  29177  upgredgpr  29211  numedglnl  29213  usgrausgrb  29238  usgrnloopvALT  29270  usgrnloopALT  29272  usgredg2vlem2  29295  ushgredgedg  29298  ushgredgedgloop  29300  upgrreslem  29373  umgrreslem  29374  nbgr0edglem  29425  nbusgrvtxm1  29448  uvtxnbgrvtx  29462  cusgredg  29493  cusgrres  29517  cusgrsize2inds  29522  cusgrfi  29527  fusgrregdegfi  29638  ewlkle  29674  uspgr2wlkeqi  29716  lfgrwlkprop  29754  lfgrwlknloop  29756  pthdivtx  29795  2pthnloop  29799  upgrwlkdvdelem  29804  upgrspthswlk  29806  usgr2wlkneq  29824  usgr2trlncl  29828  usgr2pthlem  29831  usgr2pth  29832  uspgrn2crct  29876  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0  29889  wlkiswwlks1  29935  wlkiswwlks2  29943  wlkiswwlksupgr2  29945  wwlksnred  29960  wwlksnext  29961  wwlksnextbi  29962  wwlksnextwrd  29965  wwlksnextinj  29967  wwlksnextproplem2  29978  wwlksnextproplem3  29979  wspthsnonn0vne  29985  wspn0  29992  2pthon3v  30011  usgrwwlks2on  30026  umgrwwlks2on  30027  elwspths2on  30030  elwspths2onw  30031  wpthswwlks2on  30032  clwwlk1loop  30058  clwwlkccatlem  30059  umgrclwwlkge2  30061  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem3  30071  clwlkclwwlkf1lem3  30076  clwlkclwwlkfo  30079  clwwisshclwwslemlem  30083  erclwwlkeqlen  30089  erclwwlksym  30091  clwwlkf  30117  clwwlknscsh  30132  erclwwlknsym  30140  clwwlknonex2lem2  30178  clwwlknonex2  30179  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eucrctshift  30313  3vfriswmgr  30348  1to2vfriswmgr  30349  1to3vfriswmgr  30350  n4cyclfrgr  30361  4cyclusnfrgr  30362  frgrnbnb  30363  frgrncvvdeqlem8  30376  frgrwopreg  30393  frgr2wwlk1  30399  frgr2wwlkeqm  30401  2clwwlk2clwwlklem  30416  numclwwlk1lem2fo  30428  wlkl0  30437  numclwlk2lem2f  30447  frgrreggt1  30463  frgrreg  30464  frgrregord013  30465  frgrregord13  30466  frgrogt3nreg  30467  eulplig  30556  nmoub3i  30844  ipasslem5  30906  htthlem  30988  ocin  31367  spansneleq  31641  spansnss  31642  elspansn4  31644  h1datomi  31652  nmopub2tALT  31980  nmfnleub2  31997  hstel2  32290  cvnbtwn  32357  spansncv2  32364  dmdmd  32371  dmdbr3  32376  dmdbr4  32377  dmdbr5  32379  mdsl0  32381  mdexchi  32406  cvexchlem  32439  atcv1  32451  atomli  32453  atcvatlem  32456  atcvat2i  32458  chirredi  32465  mdsymlem3  32476  mdsymlem4  32477  sumdmdii  32486  sumdmdlem  32489  cdj1i  32504  ssrelf  32688  f1o3d  32699  fisshasheq  35297  umgr2cycllem  35322  cvxpconn  35424  satfv0  35540  satfsschain  35546  satfrel  35549  satfdm  35551  satfv0fun  35553  sat1el2xp  35561  gonarlem  35576  goalrlem  35578  satffunlem1lem1  35584  satffunlem2lem1  35586  satffunlem2lem2  35588  satffun  35591  mrsubccat  35700  msubvrs  35742  fundmpss  35949  dfon2lem6  35968  dfon2lem8  35970  dfon2lem9  35971  dfon2  35972  wzel  36004  colinearxfr  36257  btwnconn1lem11  36279  lineintmo  36339  in-ax8  36406  ss-ax8  36407  trer  36498  elicc3  36499  finminlem  36500  nn0prpwlem  36504  fnessref  36539  neibastop2  36543  fgmin  36552  tailfb  36559  ordcmp  36629  ee7.2aOLD  36643  dfttc4  36712  bj-ceqsalt0  37191  bj-ceqsalt1  37192  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlpssretop  37680  fvineqsneu  37727  fvineqsneq  37728  wl-mo3t  37901  finixpnum  37926  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  ftc1anc  38022  fdc  38066  heibor1lem  38130  ghomco  38212  rngoueqz  38261  unichnidl  38352  dmncan1  38397  ax12indn  39389  lshpdisj  39433  lub0N  39635  glb0N  39639  leat2  39740  hlrelat2  39849  cvrexchlem  39865  cvratlem  39867  atcvrj0  39874  cvrat2  39875  snatpsubN  40196  linepsubN  40198  pmaple  40207  pmapsub  40214  elpaddn0  40246  paddasslem5  40270  trlval2  40609  cdlemn11pre  41656  dihord2pre  41671  mapdordlem2  42083  sn-sup2  42936  fsuppind  43023  pell1qrgap  43302  dford3lem1  43454  hbtlem5  43556  onexlimgt  43671  onsucf1olem  43698  omcl2  43761  tfsconcat0b  43774  ntrneiiso  44518  sbiota1  44861  19.41rg  44977  ee223  45061  or2expropbilem1  47480  funressnfv  47491  fcoresf1  47517  2reuimp  47563  f1oresf1o2  47739  zm1nn  47750  nltle2tri  47761  el1fzopredsuc  47774  modlt0b  47817  mod2addne  47818  muldvdsfacgt  47834  muldvdsfacm1  47835  elsetpreimafvssdm  47846  imasetpreimafvbijlemf1  47864  iccpartlt  47884  iccpartgt  47887  iccelpart  47893  icceuelpart  47896  iccpartnel  47898  fargshiftfo  47902  fargshiftfva  47903  lswn0  47904  ich2exprop  47931  prsprel  47947  sprsymrelfolem2  47953  sprsymrelfo  47957  poprelb  47984  reuopreuprim  47986  goldbachthlem2  48009  odz2prm2pw  48026  fmtnoprmfac1  48028  fmtnofac2lem  48031  prmdvdsfmtnof1lem2  48048  2pwp1prm  48052  sfprmdvdsmersenne  48066  lighneallem3  48070  requad01  48097  requad2  48099  even3prm2  48195  fppr2odd  48207  fpprwpprb  48216  gbegt5  48237  sbgoldbwt  48253  sbgoldbalt  48257  sbgoldbm  48260  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgblthelfgott  48291  tgoldbach  48293  isubgredg  48342  grimuhgr  48363  grimcnv  48364  grimco  48365  isuspgrim0  48370  isuspgrimlem  48371  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409  grimedg  48411  grtriprop  48417  cycl3grtri  48423  grimgrtri  48425  isubgr3stgrlem6  48447  uspgrlimlem3  48466  uspgrlimlem4  48467  grlimgrtrilem2  48478  grlicsym  48489  clnbgr3stgrgrlim  48495  clnbgr3stgrgrlic  48496  gpgedg2ov  48542  gpgedg2iv  48543  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  upgrwlkupwlk  48616  lmod0rng  48705  ztprmneprm  48823  ply1mulgsumlem1  48862  ply1mulgsumlem2  48863  lcoel0  48904  linindslinci  48924  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  snlindsntor  48947  ldepspr  48949  lincresunit2  48954  fllog2  49044  dignn0ldlem  49078  dignn0flhalflem1  49091  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  itcovalt2  49153  resum2sqorgt0  49185  eenglngeehlnmlem2  49214  rrx2linest  49218  itscnhlc0xyqsol  49241  itsclc0  49247  setrec1lem2  50163  aacllem  50276