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  844  dedlem0b  1045  sbequ1  2249  moexexlem  2629  ralrimdvva  3217  ceqsal1t  3522  ceqsalt  3523  spcimgft  3558  vtoclgft  3564  elabgt  3685  sbciegftOLD  3843  reupick  4348  reusv3  5423  sbcop1  5508  propeqop  5526  pwssun  5590  wefrc  5694  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  ssrelrn  5919  tz7.7  6421  ordtr2  6439  onmindif  6487  unizlim  6518  funssres  6622  f1ssf1  6894  fvmptt  7049  fveqdmss  7112  fvcofneq  7127  funsndifnop  7185  funfvima2  7268  isoini  7374  isopolem  7381  weniso  7390  f1ocnv2d  7703  limsssuc  7887  tfindsg  7898  limomss  7908  findsg  7937  funcnvuni  7972  f1oweALT  8013  funelss  8088  bropopvvv  8131  bropfvvvvlem  8132  bropfvvvv  8133  f1o2ndf1  8163  frxp  8167  soseq  8200  suppfnss  8230  wfrlem12OLD  8376  onfununi  8397  tz7.49  8501  omordi  8622  omlimcl  8634  omass  8636  oeordsuc  8650  nnmordi  8687  nnmord  8688  omabs  8707  xpdom2  9133  infensuc  9221  findcard2  9230  findcard2d  9232  findcard3  9346  findcard3OLD  9347  frfi  9349  xpfiOLD  9387  fsuppres  9462  dffi2  9492  elfiun  9499  ordiso2  9584  ordtypelem7  9593  suc11reg  9688  inf3lem2  9698  noinfep  9729  cantnfle  9740  cantnflem1  9758  cantnf  9762  ttrclss  9789  trcl  9797  epfrs  9800  frr3g  9825  r1sdom  9843  updjud  10003  pr2neOLD  10074  dfac8alem  10098  indcardi  10110  alephordi  10143  dfac12lem3  10215  pwsdompw  10272  cofsmo  10338  cfcoflem  10341  coftr  10342  isf32lem2  10423  isf32lem9  10430  axcc3  10507  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  zorn2lem4  10568  zorn2lem6  10570  zorn2lem7  10571  ttukeylem6  10583  uniimadom  10613  konigthlem  10637  fpwwe2lem7  10706  tskord  10849  tskcard  10850  grupr  10866  gruiin  10879  grudomon  10886  grur1a  10888  genpn0  11072  genpcd  11075  distrlem5pr  11096  psslinpr  11100  ltaddpr  11103  ltexprlem3  11107  ltexprlem6  11110  ltapr  11114  prlem936  11116  suplem1pr  11121  axpre-sup  11238  1re  11290  dedekindle  11454  lemul12a  12152  divgt0  12163  divge0  12164  lbreu  12245  sup2  12251  bndndx  12552  elnnz  12649  nzadd  12691  fzind  12741  fnn0ind  12742  uzwo  12976  lbzbi  13001  zmax  13010  zbtwnre  13011  irradd  13038  irrmul  13039  ledivge1le  13128  xrub  13374  supxrunb2  13382  infmremnf  13405  iccid  13452  uzsubsubfz  13606  fzrevral  13669  elfz0fzfz0  13690  fz0fzelfz0  13691  elfzmlbp  13696  elincfzoext  13774  ssfzoulel  13810  ssfzo12bi  13811  fzoopth  13812  elfzonelfzo  13819  elfznelfzo  13822  elfznelfzob  13823  injresinjlem  13837  fleqceilz  13905  modaddmodup  13985  uzindi  14033  suppssfz  14045  mptnn0fsuppr  14050  le2sq2  14185  sqlecan  14258  facdiv  14336  facwordi  14338  faclbnd  14339  hashimarni  14490  hash2prd  14524  hashle2pr  14526  pr2pwpr  14528  fundmge2nop0  14551  fi1uzind  14556  brfi1indALT  14559  swrdnd2  14703  swrdnnn0nd  14704  swrdnd0  14705  pfxnd0  14736  swrdswrdlem  14752  swrdswrd  14753  ccatopth2  14765  wrd2ind  14771  pfxccatin12lem2a  14775  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12lem3  14780  swrdccat  14783  swrdccat3blem  14787  reuccatpfxs1lem  14794  repswswrd  14832  cshwidxmod  14851  cshwidx0  14854  2cshwcshw  14874  cshwcsh2id  14877  cau3lem  15403  caubnd  15407  climrlim2  15593  rlimcn3  15636  mulcn2  15642  climcau  15719  climbdd  15720  caucvg  15727  modfsummod  15842  p1modz1  16309  dvdsle  16358  dvdsdivcl  16364  ltoddhalfle  16409  halfleoddlt  16410  ndvdssub  16457  gcdcllem1  16545  dvdslegcd  16550  bezoutlem4  16589  dfgcd2  16593  lcmf  16680  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem  16688  lcmfdvdsb  16690  lcmfun  16692  coprmdvds1  16699  divgcdcoprm0  16712  cncongr1  16714  cncongr2  16715  prmfac1  16767  pcqcl  16903  dvdsprmpweqle  16933  oddprmdvds  16950  prmpwdvds  16951  infpnlem1  16957  prmgaplem5  17102  prmgaplem6  17103  prmgaplem7  17104  cshwshashlem1  17143  cictr  17866  initoeu2lem1  18081  initoeu2  18083  clatleglb  18588  lidrididd  18708  mulgaddcom  19138  mulginvcom  19139  cycsubm  19242  cyccom  19243  gsmsymgreqlem2  19473  symggen  19512  psgnunilem4  19539  sylow2blem3  19664  frgpnabllem1  19915  imasabl  19918  dprddisj2  20083  lmodfopnelem1  20918  lssssr  20975  lss1d  20984  lspsncv0  21171  rnglidlmcl  21249  rngqiprngimfo  21334  nzerooringczr  21514  pzriprnglem5  21519  pzriprnglem8  21522  znrrg  21607  mplcoe5lem  22080  cply1mul  22321  coe1fzgsumdlem  22328  gsummoncoe1  22333  evl1gsumdlem  22381  mamufacex  22421  dmatelnd  22523  scmataddcl  22543  scmatsubcl  22544  scmatmulcl  22545  smatvscl  22551  mavmulsolcl  22578  mdetdiagid  22627  cramerlem3  22716  pmatcoe1fsupp  22728  cpmatacl  22743  cpmatmcllem  22745  mp2pm2mplem4  22836  chpscmat  22869  chfacfisf  22881  chfacfisfcpmat  22882  uniopn  22924  opnnei  23149  neindisj2  23152  restcls  23210  restntr  23211  tgcnp  23282  subbascn  23283  iscnp4  23292  lpcls  23393  cmpsublem  23428  cmpsub  23429  tgcmp  23430  cmpcld  23431  dfconn2  23448  1stcrest  23482  2ndcdisj  23485  1stccnp  23491  comppfsc  23561  kgencn2  23586  txlm  23677  kqreglem1  23770  filin  23883  isfil2  23885  ufilmax  23936  ufileu  23948  filufint  23949  cfinufil  23957  elfm2  23977  rnelfmlem  23981  rnelfm  23982  flimopn  24004  fbflim2  24006  flffbas  24024  fclsnei  24048  flimfnfcls  24057  fclscmp  24059  fcfnei  24064  cnpfcf  24070  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  ptcmplem4  24084  qustgplem  24150  tsmsres  24173  tsmsxp  24184  metss  24542  metcnp3  24574  ovoliunnul  25561  ovolicc2lem3  25573  dyadmax  25652  itg2le  25794  bddiblnc  25897  itgcn  25900  ellimc3  25934  lhop1  26073  dvfsumrlim  26092  fta1g  26229  dvply2g  26344  fta1  26368  aalioulem3  26394  aalioulem4  26395  ulmcaulem  26455  ulmcau  26456  logbgcd1irr  26855  xrlimcnp  27029  cxploglim  27039  jensen  27050  lgsqrmodndvds  27415  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem3  27430  lgsquad2lem2  27447  2lgslem1a1  27451  2sqlem6  27485  2sq2  27495  2sqnn  27501  2sqreultblem  27510  nosepdmlem  27746  nodenselem8  27754  madebdaylemlrcut  27955  addsprop  28027  addsuniflem  28052  negsprop  28085  mulsprop  28174  mulsuniflem  28193  precsex  28260  elnnzs  28405  brbtwn2  28938  ax5seglem5  28966  axcontlem4  29000  axcontlem10  29006  umgrnloopv  29141  umgrnloop  29143  upgredgpr  29177  numedglnl  29179  usgrausgrb  29204  usgrnloopvALT  29236  usgrnloopALT  29238  usgredg2vlem2  29261  ushgredgedg  29264  ushgredgedgloop  29266  upgrreslem  29339  umgrreslem  29340  nbgr0edglem  29391  nbusgrvtxm1  29414  uvtxnbgrvtx  29428  cusgredg  29459  cusgrres  29484  cusgrsize2inds  29489  cusgrfi  29494  fusgrregdegfi  29605  ewlkle  29641  uspgr2wlkeqi  29684  lfgrwlkprop  29723  lfgrwlknloop  29725  pthdivtx  29765  2pthnloop  29767  upgrwlkdvdelem  29772  upgrspthswlk  29774  usgr2wlkneq  29792  usgr2trlncl  29796  usgr2pthlem  29799  usgr2pth  29800  uspgrn2crct  29841  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0  29854  wlkiswwlks1  29900  wlkiswwlks2  29908  wlkiswwlksupgr2  29910  wwlksnred  29925  wwlksnext  29926  wwlksnextbi  29927  wwlksnextwrd  29930  wwlksnextinj  29932  wwlksnextproplem2  29943  wwlksnextproplem3  29944  wspthsnonn0vne  29950  wspn0  29957  2pthon3v  29976  umgrwwlks2on  29990  elwspths2on  29993  wpthswwlks2on  29994  clwwlk1loop  30020  clwwlkccatlem  30021  umgrclwwlkge2  30023  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem3  30033  clwlkclwwlkf1lem3  30038  clwlkclwwlkfo  30041  clwwisshclwwslemlem  30045  erclwwlkeqlen  30051  erclwwlksym  30053  clwwlkf  30079  clwwlknscsh  30094  erclwwlknsym  30102  clwwlknonex2lem2  30140  clwwlknonex2  30141  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eucrctshift  30275  3vfriswmgr  30310  1to2vfriswmgr  30311  1to3vfriswmgr  30312  n4cyclfrgr  30323  4cyclusnfrgr  30324  frgrnbnb  30325  frgrncvvdeqlem8  30338  frgrwopreg  30355  frgr2wwlk1  30361  frgr2wwlkeqm  30363  2clwwlk2clwwlklem  30378  numclwwlk1lem2fo  30390  wlkl0  30399  numclwlk2lem2f  30409  frgrreggt1  30425  frgrreg  30426  frgrregord013  30427  frgrregord13  30428  frgrogt3nreg  30429  eulplig  30517  nmoub3i  30805  ipasslem5  30867  htthlem  30949  ocin  31328  spansneleq  31602  spansnss  31603  elspansn4  31605  h1datomi  31613  nmopub2tALT  31941  nmfnleub2  31958  hstel2  32251  cvnbtwn  32318  spansncv2  32325  dmdmd  32332  dmdbr3  32337  dmdbr4  32338  dmdbr5  32340  mdsl0  32342  mdexchi  32367  cvexchlem  32400  atcv1  32412  atomli  32414  atcvatlem  32417  atcvat2i  32419  chirredi  32426  mdsymlem3  32437  mdsymlem4  32438  sumdmdii  32447  sumdmdlem  32450  cdj1i  32465  ssrelf  32637  f1o3d  32646  fisshasheq  35082  umgr2cycllem  35108  cvxpconn  35210  satfv0  35326  satfsschain  35332  satfrel  35335  satfdm  35337  satfv0fun  35339  sat1el2xp  35347  gonarlem  35362  goalrlem  35364  satffunlem1lem1  35370  satffunlem2lem1  35372  satffunlem2lem2  35374  satffun  35377  mrsubccat  35486  msubvrs  35528  fundmpss  35730  dfon2lem6  35752  dfon2lem8  35754  dfon2lem9  35755  dfon2  35756  wzel  35788  colinearxfr  36039  btwnconn1lem11  36061  lineintmo  36121  in-ax8  36190  ss-ax8  36191  trer  36282  elicc3  36283  finminlem  36284  nn0prpwlem  36288  fnessref  36323  neibastop2  36327  fgmin  36336  tailfb  36343  ordcmp  36413  ee7.2aOLD  36427  bj-cbvalimt  36605  bj-ceqsalt0  36850  bj-ceqsalt1  36851  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlpssretop  37330  fvineqsneu  37377  fvineqsneq  37378  wl-mo3t  37530  finixpnum  37565  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  ftc1anc  37661  fdc  37705  heibor1lem  37769  ghomco  37851  rngoueqz  37900  unichnidl  37991  dmncan1  38036  ax12indn  38899  lshpdisj  38943  lub0N  39145  glb0N  39149  leat2  39250  hlrelat2  39360  cvrexchlem  39376  cvratlem  39378  atcvrj0  39385  cvrat2  39386  snatpsubN  39707  linepsubN  39709  pmaple  39718  pmapsub  39725  elpaddn0  39757  paddasslem5  39781  trlval2  40120  cdlemn11pre  41167  dihord2pre  41182  mapdordlem2  41594  sn-sup2  42447  fsuppind  42545  pell1qrgap  42830  dford3lem1  42983  hbtlem5  43085  onexlimgt  43204  onsucf1olem  43232  omcl2  43295  tfsconcat0b  43308  ntrneiiso  44053  sbiota1  44403  19.41rg  44521  ee223  44605  or2expropbilem1  46947  funressnfv  46958  fcoresf1  46984  2reuimp  47030  f1oresf1o2  47206  zm1nn  47217  nltle2tri  47228  el1fzopredsuc  47240  elsetpreimafvssdm  47260  imasetpreimafvbijlemf1  47278  iccpartlt  47298  iccpartgt  47301  iccelpart  47307  icceuelpart  47310  iccpartnel  47312  fargshiftfo  47316  fargshiftfva  47317  lswn0  47318  ich2exprop  47345  prsprel  47361  sprsymrelfolem2  47367  sprsymrelfo  47371  poprelb  47398  reuopreuprim  47400  goldbachthlem2  47420  odz2prm2pw  47437  fmtnoprmfac1  47439  fmtnofac2lem  47442  prmdvdsfmtnof1lem2  47459  2pwp1prm  47463  sfprmdvdsmersenne  47477  lighneallem3  47481  requad01  47495  requad2  47497  even3prm2  47593  fppr2odd  47605  fpprwpprb  47614  gbegt5  47635  sbgoldbwt  47651  sbgoldbalt  47655  sbgoldbm  47658  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  tgblthelfgott  47689  tgoldbach  47691  isuspgrim0  47756  isuspgrimlem  47758  grimuhgr  47762  grimcnv  47763  grimco  47764  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785  grimedg  47787  grtriprop  47792  grimgrtri  47798  uspgrlimlem3  47814  uspgrlimlem4  47815  grlimgrtrilem2  47819  grlicsym  47830  upgrwlkupwlk  47863  lmod0rng  47952  ztprmneprm  48072  ply1mulgsumlem1  48115  ply1mulgsumlem2  48116  lcoel0  48157  linindslinci  48177  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  snlindsntor  48200  ldepspr  48202  lincresunit2  48207  fllog2  48302  dignn0ldlem  48336  dignn0flhalflem1  48349  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  itcovalt2  48411  resum2sqorgt0  48443  eenglngeehlnmlem2  48472  rrx2linest  48476  itscnhlc0xyqsol  48499  itsclc0  48505  setrec1lem2  48780  aacllem  48895