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  410  expcomd  415  impancom  450  a2and  843  dedlem0b  1042  sbequ1  2236  moexexlem  2615  ralrimdvva  3200  ceqsal1t  3495  ceqsalt  3496  vtoclgft  3532  elabgt  3659  sbciegftOLD  3815  reupick  4321  reusv3  5411  sbcop1  5496  propeqop  5515  pwssun  5579  wefrc  5678  ssrel  5790  ssrelOLD  5791  ssrel2  5793  ssrelrel  5804  ssrelrn  5903  tz7.7  6404  ordtr2  6422  onmindif  6470  unizlim  6501  funssres  6605  f1ssf1  6877  fvmptt  7031  fveqdmss  7094  fvcofneq  7109  funsndifnop  7167  funfvima2  7250  isoini  7352  isopolem  7359  weniso  7368  f1ocnv2d  7681  limsssuc  7862  tfindsg  7873  limomss  7883  findsg  7912  funcnvuni  7947  f1oweALT  7988  funelss  8063  bropopvvv  8106  bropfvvvvlem  8107  bropfvvvv  8108  f1o2ndf1  8138  frxp  8142  soseq  8175  suppfnss  8205  wfrlem12OLD  8352  onfununi  8373  tz7.49  8477  omordi  8598  omlimcl  8610  omass  8612  oeordsuc  8626  nnmordi  8663  nnmord  8664  omabs  8683  xpdom2  9107  infensuc  9195  findcard2  9204  findcard2d  9206  findcard2OLD  9320  findcard3  9321  findcard3OLD  9322  frfi  9324  xpfiOLD  9363  fsuppres  9438  dffi2  9468  elfiun  9475  ordiso2  9560  ordtypelem7  9569  suc11reg  9664  inf3lem2  9674  noinfep  9705  cantnfle  9716  cantnflem1  9734  cantnf  9738  ttrclss  9765  trcl  9773  epfrs  9776  frr3g  9801  r1sdom  9819  updjud  9979  pr2neOLD  10050  dfac8alem  10074  indcardi  10086  alephordi  10119  dfac12lem3  10190  pwsdompw  10249  cofsmo  10314  cfcoflem  10317  coftr  10318  isf32lem2  10399  isf32lem9  10406  axcc3  10483  domtriomlem  10487  axdc3lem2  10496  axdc3lem4  10498  zorn2lem4  10544  zorn2lem6  10546  zorn2lem7  10547  ttukeylem6  10559  uniimadom  10589  konigthlem  10613  fpwwe2lem7  10682  tskord  10825  tskcard  10826  grupr  10842  gruiin  10855  grudomon  10862  grur1a  10864  genpn0  11048  genpcd  11051  distrlem5pr  11072  psslinpr  11076  ltaddpr  11079  ltexprlem3  11083  ltexprlem6  11086  ltapr  11090  prlem936  11092  suplem1pr  11097  axpre-sup  11214  1re  11266  dedekindle  11430  lemul12a  12125  divgt0  12136  divge0  12137  lbreu  12218  sup2  12224  bndndx  12525  elnnz  12622  nzadd  12664  fzind  12714  fnn0ind  12715  uzwo  12949  lbzbi  12974  zmax  12983  zbtwnre  12984  irradd  13011  irrmul  13012  ledivge1le  13101  xrub  13347  supxrunb2  13355  infmremnf  13378  iccid  13425  uzsubsubfz  13579  fzrevral  13642  elfz0fzfz0  13662  fz0fzelfz0  13663  elfzmlbp  13668  elincfzoext  13746  ssfzoulel  13782  ssfzo12bi  13783  fzoopth  13784  elfzonelfzo  13791  elfznelfzo  13794  elfznelfzob  13795  injresinjlem  13809  fleqceilz  13876  modaddmodup  13956  uzindi  14004  suppssfz  14016  mptnn0fsuppr  14021  le2sq2  14156  sqlecan  14229  facdiv  14306  facwordi  14308  faclbnd  14309  hashimarni  14460  hash2prd  14496  hashle2pr  14498  pr2pwpr  14500  fundmge2nop0  14513  fi1uzind  14518  brfi1indALT  14521  swrdnd2  14665  swrdnnn0nd  14666  swrdnd0  14667  pfxnd0  14698  swrdswrdlem  14714  swrdswrd  14715  ccatopth2  14727  wrd2ind  14733  pfxccatin12lem2a  14737  swrdccatin2  14739  pfxccatin12lem2  14741  pfxccatin12lem3  14742  swrdccat  14745  swrdccat3blem  14749  reuccatpfxs1lem  14756  repswswrd  14794  cshwidxmod  14813  cshwidx0  14816  2cshwcshw  14836  cshwcsh2id  14839  cau3lem  15361  caubnd  15365  climrlim2  15551  rlimcn3  15594  mulcn2  15600  climcau  15677  climbdd  15678  caucvg  15685  modfsummod  15800  p1modz1  16265  dvdsle  16314  dvdsdivcl  16320  ltoddhalfle  16365  halfleoddlt  16366  ndvdssub  16413  gcdcllem1  16501  dvdslegcd  16506  bezoutlem4  16545  dfgcd2  16549  lcmf  16636  lcmfunsnlem1  16640  lcmfunsnlem2lem1  16641  lcmfunsnlem  16644  lcmfdvdsb  16646  lcmfun  16648  coprmdvds1  16655  divgcdcoprm0  16668  cncongr1  16670  cncongr2  16671  prmfac1  16724  pcqcl  16860  dvdsprmpweqle  16890  oddprmdvds  16907  prmpwdvds  16908  infpnlem1  16914  prmgaplem5  17059  prmgaplem6  17060  prmgaplem7  17061  cshwshashlem1  17100  cictr  17823  initoeu2lem1  18038  initoeu2  18040  clatleglb  18545  lidrididd  18665  mulgaddcom  19094  mulginvcom  19095  cycsubm  19198  cyccom  19199  gsmsymgreqlem2  19431  symggen  19470  psgnunilem4  19497  sylow2blem3  19622  frgpnabllem1  19873  imasabl  19876  dprddisj2  20041  lmodfopnelem1  20876  lssssr  20933  lss1d  20942  lspsncv0  21129  rnglidlmcl  21207  rngqiprngimfo  21292  nzerooringczr  21472  pzriprnglem5  21477  pzriprnglem8  21480  znrrg  21565  mplcoe5lem  22048  cply1mul  22290  coe1fzgsumdlem  22297  gsummoncoe1  22302  evl1gsumdlem  22350  mamufacex  22390  dmatelnd  22492  scmataddcl  22512  scmatsubcl  22513  scmatmulcl  22514  smatvscl  22520  mavmulsolcl  22547  mdetdiagid  22596  cramerlem3  22685  pmatcoe1fsupp  22697  cpmatacl  22712  cpmatmcllem  22714  mp2pm2mplem4  22805  chpscmat  22838  chfacfisf  22850  chfacfisfcpmat  22851  uniopn  22893  opnnei  23118  neindisj2  23121  restcls  23179  restntr  23180  tgcnp  23251  subbascn  23252  iscnp4  23261  lpcls  23362  cmpsublem  23397  cmpsub  23398  tgcmp  23399  cmpcld  23400  dfconn2  23417  1stcrest  23451  2ndcdisj  23454  1stccnp  23460  comppfsc  23530  kgencn2  23555  txlm  23646  kqreglem1  23739  filin  23852  isfil2  23854  ufilmax  23905  ufileu  23917  filufint  23918  cfinufil  23926  elfm2  23946  rnelfmlem  23950  rnelfm  23951  flimopn  23973  fbflim2  23975  flffbas  23993  fclsnei  24017  flimfnfcls  24026  fclscmp  24028  fcfnei  24033  cnpfcf  24039  alexsubALTlem2  24046  alexsubALTlem3  24047  alexsubALTlem4  24048  alexsubALT  24049  ptcmplem4  24053  qustgplem  24119  tsmsres  24142  tsmsxp  24153  metss  24511  metcnp3  24543  ovoliunnul  25530  ovolicc2lem3  25542  dyadmax  25621  itg2le  25763  bddiblnc  25865  itgcn  25868  ellimc3  25902  lhop1  26041  dvfsumrlim  26060  fta1g  26200  dvply2g  26315  fta1  26339  aalioulem3  26365  aalioulem4  26366  ulmcaulem  26426  ulmcau  26427  logbgcd1irr  26825  xrlimcnp  26999  cxploglim  27009  jensen  27020  lgsqrmodndvds  27385  gausslemma2dlem1a  27397  gausslemma2dlem2  27399  gausslemma2dlem3  27400  lgsquad2lem2  27417  2lgslem1a1  27421  2sqlem6  27455  2sq2  27465  2sqnn  27471  2sqreultblem  27480  nosepdmlem  27716  nodenselem8  27724  madebdaylemlrcut  27925  addsprop  27993  addsuniflem  28018  negsprop  28047  mulsprop  28134  mulsuniflem  28153  precsex  28220  brbtwn2  28842  ax5seglem5  28870  axcontlem4  28904  axcontlem10  28910  umgrnloopv  29045  umgrnloop  29047  upgredgpr  29081  numedglnl  29083  usgrausgrb  29108  usgrnloopvALT  29140  usgrnloopALT  29142  usgredg2vlem2  29165  ushgredgedg  29168  ushgredgedgloop  29170  upgrreslem  29243  umgrreslem  29244  nbgr0edglem  29295  nbusgrvtxm1  29318  uvtxnbgrvtx  29332  cusgredg  29363  cusgrres  29388  cusgrsize2inds  29393  cusgrfi  29398  fusgrregdegfi  29509  ewlkle  29545  uspgr2wlkeqi  29588  lfgrwlkprop  29627  lfgrwlknloop  29629  pthdivtx  29669  2pthnloop  29671  upgrwlkdvdelem  29676  upgrspthswlk  29678  usgr2wlkneq  29696  usgr2trlncl  29700  usgr2pthlem  29703  usgr2pth  29704  uspgrn2crct  29745  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0  29758  wlkiswwlks1  29804  wlkiswwlks2  29812  wlkiswwlksupgr2  29814  wwlksnred  29829  wwlksnext  29830  wwlksnextbi  29831  wwlksnextwrd  29834  wwlksnextinj  29836  wwlksnextproplem2  29847  wwlksnextproplem3  29848  wspthsnonn0vne  29854  wspn0  29861  2pthon3v  29880  umgrwwlks2on  29894  elwspths2on  29897  wpthswwlks2on  29898  clwwlk1loop  29924  clwwlkccatlem  29925  umgrclwwlkge2  29927  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem3  29937  clwlkclwwlkf1lem3  29942  clwlkclwwlkfo  29945  clwwisshclwwslemlem  29949  erclwwlkeqlen  29955  erclwwlksym  29957  clwwlkf  29983  clwwlknscsh  29998  erclwwlknsym  30006  clwwlknonex2lem2  30044  clwwlknonex2  30045  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eucrctshift  30179  3vfriswmgr  30214  1to2vfriswmgr  30215  1to3vfriswmgr  30216  n4cyclfrgr  30227  4cyclusnfrgr  30228  frgrnbnb  30229  frgrncvvdeqlem8  30242  frgrwopreg  30259  frgr2wwlk1  30265  frgr2wwlkeqm  30267  2clwwlk2clwwlklem  30282  numclwwlk1lem2fo  30294  wlkl0  30303  numclwlk2lem2f  30313  frgrreggt1  30329  frgrreg  30330  frgrregord013  30331  frgrregord13  30332  frgrogt3nreg  30333  eulplig  30421  nmoub3i  30709  ipasslem5  30771  htthlem  30853  ocin  31232  spansneleq  31506  spansnss  31507  elspansn4  31509  h1datomi  31517  nmopub2tALT  31845  nmfnleub2  31862  hstel2  32155  cvnbtwn  32222  spansncv2  32229  dmdmd  32236  dmdbr3  32241  dmdbr4  32242  dmdbr5  32244  mdsl0  32246  mdexchi  32271  cvexchlem  32304  atcv1  32316  atomli  32318  atcvatlem  32321  atcvat2i  32323  chirredi  32330  mdsymlem3  32341  mdsymlem4  32342  sumdmdii  32351  sumdmdlem  32354  cdj1i  32369  ssrelf  32537  f1o3d  32546  fisshasheq  34944  umgr2cycllem  34970  cvxpconn  35072  satfv0  35188  satfsschain  35194  satfrel  35197  satfdm  35199  satfv0fun  35201  sat1el2xp  35209  gonarlem  35224  goalrlem  35226  satffunlem1lem1  35232  satffunlem2lem1  35234  satffunlem2lem2  35236  satffun  35239  mrsubccat  35348  msubvrs  35390  fundmpss  35592  dfon2lem6  35614  dfon2lem8  35616  dfon2lem9  35617  dfon2  35618  wzel  35650  colinearxfr  35901  btwnconn1lem11  35923  lineintmo  35983  trer  36030  elicc3  36031  finminlem  36032  nn0prpwlem  36036  fnessref  36071  neibastop2  36075  fgmin  36084  tailfb  36091  ordcmp  36161  ee7.2aOLD  36175  bj-cbvalimt  36345  bj-ceqsalt0  36592  bj-ceqsalt1  36593  isbasisrelowllem1  37064  isbasisrelowllem2  37065  relowlpssretop  37073  fvineqsneu  37120  fvineqsneq  37121  wl-mo3t  37273  finixpnum  37308  matunitlindflem1  37319  matunitlindflem2  37320  poimirlem26  37349  poimirlem27  37350  poimirlem29  37352  ftc1anc  37404  fdc  37448  heibor1lem  37512  ghomco  37594  rngoueqz  37643  unichnidl  37734  dmncan1  37779  ax12indn  38643  lshpdisj  38687  lub0N  38889  glb0N  38893  leat2  38994  hlrelat2  39104  cvrexchlem  39120  cvratlem  39122  atcvrj0  39129  cvrat2  39130  snatpsubN  39451  linepsubN  39453  pmaple  39462  pmapsub  39469  elpaddn0  39501  paddasslem5  39525  trlval2  39864  cdlemn11pre  40911  dihord2pre  40926  mapdordlem2  41338  sn-sup2  42162  fsuppind  42260  pell1qrgap  42549  dford3lem1  42702  hbtlem5  42807  onexlimgt  42926  onsucf1olem  42954  omcl2  43017  tfsconcat0b  43030  ntrneiiso  43776  sbiota1  44126  19.41rg  44244  ee223  44328  or2expropbilem1  46665  funressnfv  46676  fcoresf1  46702  2reuimp  46746  f1oresf1o2  46922  zm1nn  46933  nltle2tri  46944  el1fzopredsuc  46956  elsetpreimafvssdm  46976  imasetpreimafvbijlemf1  46994  iccpartlt  47014  iccpartgt  47017  iccelpart  47023  icceuelpart  47026  iccpartnel  47028  fargshiftfo  47032  fargshiftfva  47033  lswn0  47034  ich2exprop  47061  prsprel  47077  sprsymrelfolem2  47083  sprsymrelfo  47087  poprelb  47114  reuopreuprim  47116  goldbachthlem2  47136  odz2prm2pw  47153  fmtnoprmfac1  47155  fmtnofac2lem  47158  prmdvdsfmtnof1lem2  47175  2pwp1prm  47179  sfprmdvdsmersenne  47193  lighneallem3  47197  requad01  47211  requad2  47213  even3prm2  47309  fppr2odd  47321  fpprwpprb  47330  gbegt5  47351  sbgoldbwt  47367  sbgoldbalt  47371  sbgoldbm  47374  bgoldbtbndlem2  47396  bgoldbtbndlem3  47397  bgoldbtbndlem4  47398  bgoldbtbnd  47399  tgblthelfgott  47405  tgoldbach  47407  isuspgrim0  47469  isuspgrimlem  47471  grimuhgr  47475  grimcnv  47476  grimco  47477  uhgrimisgrgriclem  47495  clnbgrgrimlem  47498  grlicsym  47521  upgrwlkupwlk  47535  lmod0rng  47624  ztprmneprm  47744  ply1mulgsumlem1  47787  ply1mulgsumlem2  47788  lcoel0  47829  linindslinci  47849  lindslinindimp2lem4  47862  lindslinindsimp2lem5  47863  snlindsntor  47872  ldepspr  47874  lincresunit2  47879  fllog2  47974  dignn0ldlem  48008  dignn0flhalflem1  48021  nn0sumshdiglemA  48025  nn0sumshdiglemB  48026  itcovalt2  48083  resum2sqorgt0  48115  eenglngeehlnmlem2  48144  rrx2linest  48148  itscnhlc0xyqsol  48171  itsclc0  48177  setrec1lem2  48452  aacllem  48567