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  845  dedlem0b  1044  sbequ1  2255  moexexlem  2626  ralrimdvva  3191  ceqsal1t  3473  ceqsalt  3474  spcimgft  3503  vtoclgft  3509  elabgtOLD  3627  sbciegftOLD  3778  reupick  4281  reusv3  5350  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  6961  fveqdmss  7023  fvcofneq  7038  funsndifnop  7096  funfvima2  7177  isoini  7284  isopolem  7291  weniso  7300  f1ocnv2d  7611  limsssuc  7792  tfindsg  7803  limomss  7813  findsg  7839  funcnvuni  7874  f1oweALT  7916  funelss  7991  bropopvvv  8032  bropfvvvvlem  8033  bropfvvvv  8034  f1o2ndf1  8064  frxp  8068  soseq  8101  suppfnss  8131  onfununi  8273  tz7.49  8376  omordi  8493  omlimcl  8505  omass  8507  oeordsuc  8522  nnmordi  8559  nnmord  8560  omabs  8579  xpdom2  9000  infensuc  9083  findcard2  9089  findcard2d  9091  findcard3  9183  frfi  9185  fsuppres  9296  dffi2  9326  elfiun  9333  ordiso2  9420  ordtypelem7  9429  suc11reg  9528  inf3lem2  9538  noinfep  9569  cantnfle  9580  cantnflem1  9598  cantnf  9602  ttrclss  9629  trcl  9637  epfrs  9640  frr3g  9668  r1sdom  9686  updjud  9846  dfac8alem  9939  indcardi  9951  alephordi  9984  dfac12lem3  10056  pwsdompw  10113  cofsmo  10179  cfcoflem  10182  coftr  10183  isf32lem2  10264  isf32lem9  10271  axcc3  10348  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  zorn2lem4  10409  zorn2lem6  10411  zorn2lem7  10412  ttukeylem6  10424  uniimadom  10454  konigthlem  10479  fpwwe2lem7  10548  tskord  10691  tskcard  10692  grupr  10708  gruiin  10721  grudomon  10728  grur1a  10730  genpn0  10914  genpcd  10917  distrlem5pr  10938  psslinpr  10942  ltaddpr  10945  ltexprlem3  10949  ltexprlem6  10952  ltapr  10956  prlem936  10958  suplem1pr  10963  axpre-sup  11080  1re  11132  dedekindle  11297  lemul12a  11999  divgt0  12010  divge0  12011  lbreu  12092  sup2  12098  bndndx  12400  elnnz  12498  nzadd  12539  fzind  12590  fnn0ind  12591  uzwo  12824  lbzbi  12849  zmax  12858  zbtwnre  12859  irradd  12886  irrmul  12887  ledivge1le  12978  xrub  13227  supxrunb2  13235  infmremnf  13259  iccid  13306  uzsubsubfz  13462  fzrevral  13528  elfz0fzfz0  13549  fz0fzelfz0  13550  elfzmlbp  13555  elincfzoext  13639  ssfzoulel  13676  ssfzo12bi  13677  fzoopth  13678  elfzonelfzo  13685  elfznelfzo  13689  elfznelfzob  13690  injresinjlem  13706  fleqceilz  13774  modaddmodup  13857  uzindi  13905  suppssfz  13917  mptnn0fsuppr  13922  le2sq2  14058  sqlecan  14132  facdiv  14210  facwordi  14212  faclbnd  14213  hashimarni  14364  hash2prd  14398  hashle2pr  14400  pr2pwpr  14402  fundmge2nop0  14425  fi1uzind  14430  brfi1indALT  14433  swrdnd2  14579  swrdnnn0nd  14580  swrdnd0  14581  pfxnd0  14612  swrdswrdlem  14627  swrdswrd  14628  ccatopth2  14640  wrd2ind  14646  pfxccatin12lem2a  14650  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12lem3  14655  swrdccat  14658  swrdccat3blem  14662  reuccatpfxs1lem  14669  repswswrd  14707  cshwidxmod  14726  cshwidx0  14729  2cshwcshw  14748  cshwcsh2id  14751  cau3lem  15278  caubnd  15282  climrlim2  15470  rlimcn3  15513  mulcn2  15519  climcau  15594  climbdd  15595  caucvg  15602  modfsummod  15717  p1modz1  16186  dvdsle  16237  dvdsdivcl  16243  ltoddhalfle  16288  halfleoddlt  16289  ndvdssub  16336  gcdcllem1  16426  dvdslegcd  16431  bezoutlem4  16469  dfgcd2  16473  lcmf  16560  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem  16568  lcmfdvdsb  16570  lcmfun  16572  coprmdvds1  16579  divgcdcoprm0  16592  cncongr1  16594  cncongr2  16595  prmfac1  16647  pcqcl  16784  dvdsprmpweqle  16814  oddprmdvds  16831  prmpwdvds  16832  infpnlem1  16838  prmgaplem5  16983  prmgaplem6  16984  prmgaplem7  16985  cshwshashlem1  17023  cictr  17729  initoeu2lem1  17938  initoeu2  17940  clatleglb  18441  lidrididd  18595  mulgaddcom  19028  mulginvcom  19029  cycsubm  19131  cyccom  19132  gsmsymgreqlem2  19360  symggen  19399  psgnunilem4  19426  sylow2blem3  19551  frgpnabllem1  19802  imasabl  19805  dprddisj2  19970  lmodfopnelem1  20849  lssssr  20905  lss1d  20914  lspsncv0  21101  rnglidlmcl  21171  rngqiprngimfo  21256  nzerooringczr  21435  pzriprnglem5  21440  pzriprnglem8  21443  znrrg  21520  mplcoe5lem  21994  cply1mul  22240  coe1fzgsumdlem  22247  gsummoncoe1  22252  evl1gsumdlem  22300  mamufacex  22340  dmatelnd  22440  scmataddcl  22460  scmatsubcl  22461  scmatmulcl  22462  smatvscl  22468  mavmulsolcl  22495  mdetdiagid  22544  cramerlem3  22633  pmatcoe1fsupp  22645  cpmatacl  22660  cpmatmcllem  22662  mp2pm2mplem4  22753  chpscmat  22786  chfacfisf  22798  chfacfisfcpmat  22799  uniopn  22841  opnnei  23064  neindisj2  23067  restcls  23125  restntr  23126  tgcnp  23197  subbascn  23198  iscnp4  23207  lpcls  23308  cmpsublem  23343  cmpsub  23344  tgcmp  23345  cmpcld  23346  dfconn2  23363  1stcrest  23397  2ndcdisj  23400  1stccnp  23406  comppfsc  23476  kgencn2  23501  txlm  23592  kqreglem1  23685  filin  23798  isfil2  23800  ufilmax  23851  ufileu  23863  filufint  23864  cfinufil  23872  elfm2  23892  rnelfmlem  23896  rnelfm  23897  flimopn  23919  fbflim2  23921  flffbas  23939  fclsnei  23963  flimfnfcls  23972  fclscmp  23974  fcfnei  23979  cnpfcf  23985  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  ptcmplem4  23999  qustgplem  24065  tsmsres  24088  tsmsxp  24099  metss  24452  metcnp3  24484  ovoliunnul  25464  ovolicc2lem3  25476  dyadmax  25555  itg2le  25696  bddiblnc  25799  itgcn  25802  ellimc3  25836  lhop1  25975  dvfsumrlim  25994  fta1g  26131  dvply2g  26248  fta1  26272  aalioulem3  26298  aalioulem4  26299  ulmcaulem  26359  ulmcau  26360  logbgcd1irr  26760  xrlimcnp  26934  cxploglim  26944  jensen  26955  lgsqrmodndvds  27320  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem3  27335  lgsquad2lem2  27352  2lgslem1a1  27356  2sqlem6  27390  2sq2  27400  2sqnn  27406  2sqreultblem  27415  nosepdmlem  27651  nodenselem8  27659  eqcuts3  27800  madebdaylemlrcut  27895  addsprop  27972  addsuniflem  27997  negsprop  28031  mulsprop  28126  mulsuniflem  28145  precsex  28214  onsfi  28352  elnnzs  28397  elreno2  28491  brbtwn2  28978  ax5seglem5  29006  axcontlem4  29040  axcontlem10  29046  umgrnloopv  29179  umgrnloop  29181  upgredgpr  29215  numedglnl  29217  usgrausgrb  29242  usgrnloopvALT  29274  usgrnloopALT  29276  usgredg2vlem2  29299  ushgredgedg  29302  ushgredgedgloop  29304  upgrreslem  29377  umgrreslem  29378  nbgr0edglem  29429  nbusgrvtxm1  29452  uvtxnbgrvtx  29466  cusgredg  29497  cusgrres  29522  cusgrsize2inds  29527  cusgrfi  29532  fusgrregdegfi  29643  ewlkle  29679  uspgr2wlkeqi  29721  lfgrwlkprop  29759  lfgrwlknloop  29761  pthdivtx  29800  2pthnloop  29804  upgrwlkdvdelem  29809  upgrspthswlk  29811  usgr2wlkneq  29829  usgr2trlncl  29833  usgr2pthlem  29836  usgr2pth  29837  uspgrn2crct  29881  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0  29894  wlkiswwlks1  29940  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  wwlksnred  29965  wwlksnext  29966  wwlksnextbi  29967  wwlksnextwrd  29970  wwlksnextinj  29972  wwlksnextproplem2  29983  wwlksnextproplem3  29984  wspthsnonn0vne  29990  wspn0  29997  2pthon3v  30016  usgrwwlks2on  30031  umgrwwlks2on  30032  elwspths2on  30035  elwspths2onw  30036  wpthswwlks2on  30037  clwwlk1loop  30063  clwwlkccatlem  30064  umgrclwwlkge2  30066  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem3  30076  clwlkclwwlkf1lem3  30081  clwlkclwwlkfo  30084  clwwisshclwwslemlem  30088  erclwwlkeqlen  30094  erclwwlksym  30096  clwwlkf  30122  clwwlknscsh  30137  erclwwlknsym  30145  clwwlknonex2lem2  30183  clwwlknonex2  30184  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eucrctshift  30318  3vfriswmgr  30353  1to2vfriswmgr  30354  1to3vfriswmgr  30355  n4cyclfrgr  30366  4cyclusnfrgr  30367  frgrnbnb  30368  frgrncvvdeqlem8  30381  frgrwopreg  30398  frgr2wwlk1  30404  frgr2wwlkeqm  30406  2clwwlk2clwwlklem  30421  numclwwlk1lem2fo  30433  wlkl0  30442  numclwlk2lem2f  30452  frgrreggt1  30468  frgrreg  30469  frgrregord013  30470  frgrregord13  30471  frgrogt3nreg  30472  eulplig  30560  nmoub3i  30848  ipasslem5  30910  htthlem  30992  ocin  31371  spansneleq  31645  spansnss  31646  elspansn4  31648  h1datomi  31656  nmopub2tALT  31984  nmfnleub2  32001  hstel2  32294  cvnbtwn  32361  spansncv2  32368  dmdmd  32375  dmdbr3  32380  dmdbr4  32381  dmdbr5  32383  mdsl0  32385  mdexchi  32410  cvexchlem  32443  atcv1  32455  atomli  32457  atcvatlem  32460  atcvat2i  32462  chirredi  32469  mdsymlem3  32480  mdsymlem4  32481  sumdmdii  32490  sumdmdlem  32493  cdj1i  32508  ssrelf  32693  f1o3d  32704  fisshasheq  35309  umgr2cycllem  35334  cvxpconn  35436  satfv0  35552  satfsschain  35558  satfrel  35561  satfdm  35563  satfv0fun  35565  sat1el2xp  35573  gonarlem  35588  goalrlem  35590  satffunlem1lem1  35596  satffunlem2lem1  35598  satffunlem2lem2  35600  satffun  35603  mrsubccat  35712  msubvrs  35754  fundmpss  35961  dfon2lem6  35980  dfon2lem8  35982  dfon2lem9  35983  dfon2  35984  wzel  36016  colinearxfr  36269  btwnconn1lem11  36291  lineintmo  36351  in-ax8  36418  ss-ax8  36419  trer  36510  elicc3  36511  finminlem  36512  nn0prpwlem  36516  fnessref  36551  neibastop2  36555  fgmin  36564  tailfb  36571  ordcmp  36641  ee7.2aOLD  36655  bj-cbvalimt  36839  bj-ceqsalt0  37085  bj-ceqsalt1  37086  isbasisrelowllem1  37560  isbasisrelowllem2  37561  relowlpssretop  37569  fvineqsneu  37616  fvineqsneq  37617  wl-mo3t  37781  finixpnum  37806  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem26  37847  poimirlem27  37848  poimirlem29  37850  ftc1anc  37902  fdc  37946  heibor1lem  38010  ghomco  38092  rngoueqz  38141  unichnidl  38232  dmncan1  38277  ax12indn  39203  lshpdisj  39247  lub0N  39449  glb0N  39453  leat2  39554  hlrelat2  39663  cvrexchlem  39679  cvratlem  39681  atcvrj0  39688  cvrat2  39689  snatpsubN  40010  linepsubN  40012  pmaple  40021  pmapsub  40028  elpaddn0  40060  paddasslem5  40084  trlval2  40423  cdlemn11pre  41470  dihord2pre  41485  mapdordlem2  41897  sn-sup2  42746  fsuppind  42833  pell1qrgap  43116  dford3lem1  43268  hbtlem5  43370  onexlimgt  43485  onsucf1olem  43512  omcl2  43575  tfsconcat0b  43588  ntrneiiso  44332  sbiota1  44675  19.41rg  44791  ee223  44875  or2expropbilem1  47278  funressnfv  47289  fcoresf1  47315  2reuimp  47361  f1oresf1o2  47537  zm1nn  47548  nltle2tri  47559  el1fzopredsuc  47571  modlt0b  47609  mod2addne  47610  elsetpreimafvssdm  47632  imasetpreimafvbijlemf1  47650  iccpartlt  47670  iccpartgt  47673  iccelpart  47679  icceuelpart  47682  iccpartnel  47684  fargshiftfo  47688  fargshiftfva  47689  lswn0  47690  ich2exprop  47717  prsprel  47733  sprsymrelfolem2  47739  sprsymrelfo  47743  poprelb  47770  reuopreuprim  47772  goldbachthlem2  47792  odz2prm2pw  47809  fmtnoprmfac1  47811  fmtnofac2lem  47814  prmdvdsfmtnof1lem2  47831  2pwp1prm  47835  sfprmdvdsmersenne  47849  lighneallem3  47853  requad01  47867  requad2  47869  even3prm2  47965  fppr2odd  47977  fpprwpprb  47986  gbegt5  48007  sbgoldbwt  48023  sbgoldbalt  48027  sbgoldbm  48030  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgblthelfgott  48061  tgoldbach  48063  isubgredg  48112  grimuhgr  48133  grimcnv  48134  grimco  48135  isuspgrim0  48140  isuspgrimlem  48141  uhgrimisgrgriclem  48176  clnbgrgrimlem  48179  grimedg  48181  grtriprop  48187  cycl3grtri  48193  grimgrtri  48195  isubgr3stgrlem6  48217  uspgrlimlem3  48236  uspgrlimlem4  48237  grlimgrtrilem2  48248  grlicsym  48259  clnbgr3stgrgrlim  48265  clnbgr3stgrgrlic  48266  gpgedg2ov  48312  gpgedg2iv  48313  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  upgrwlkupwlk  48386  lmod0rng  48475  ztprmneprm  48593  ply1mulgsumlem1  48632  ply1mulgsumlem2  48633  lcoel0  48674  linindslinci  48694  lindslinindimp2lem4  48707  lindslinindsimp2lem5  48708  snlindsntor  48717  ldepspr  48719  lincresunit2  48724  fllog2  48814  dignn0ldlem  48848  dignn0flhalflem1  48861  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  itcovalt2  48923  resum2sqorgt0  48955  eenglngeehlnmlem2  48984  rrx2linest  48988  itscnhlc0xyqsol  49011  itsclc0  49017  setrec1lem2  49933  aacllem  50046