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  412  expcomd  417  impancom  452  a2and  851  dedlem0b  1050  sbequ1  2260  moexexlem  2630  ralrimdvva  3194  ceqsal1t  3463  ceqsalt  3464  spcimgft  3492  vtoclgft  3498  elabgtOLD  3611  reupick  4257  reusv3  5334  sbcop1  5428  propeqop  5448  pwssun  5510  wefrc  5612  ssrel  5726  ssrel2  5728  ssrelrel  5739  ssrelrn  5836  tz7.7  6336  ordtr2  6355  onmindif  6404  unizlim  6434  funssres  6529  f1ssf1  6799  fvmptt  6956  fveqdmss  7019  fvcofneq  7034  funsndifnop  7094  funfvima2  7175  isoini  7282  isopolem  7289  weniso  7298  f1ocnv2d  7609  limsssuc  7790  tfindsg  7801  limomss  7811  findsg  7837  funcnvuni  7872  f1oweALT  7914  funelss  7989  bropopvvv  8029  bropfvvvvlem  8030  bropfvvvv  8031  f1o2ndf1  8061  frxp  8066  soseq  8099  suppfnss  8129  onfununi  8271  tz7.49  8374  omordi  8491  omlimcl  8503  omass  8505  oeordsuc  8520  nnmordi  8557  nnmord  8558  omabs  8577  xpdom2  9000  infensuc  9083  findcard2  9089  findcard2d  9091  findcard3  9183  frfi  9185  fsuppres  9296  dffi2  9326  elfiun  9333  ordiso2  9420  ordtypelem7  9429  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  20888  lssssr  20944  lss1d  20953  lspsncv0  21139  rnglidlmcl  21209  rngqiprngimfo  21294  nzerooringczr  21455  pzriprnglem5  21460  pzriprnglem8  21463  znrrg  21540  mplcoe5lem  22015  cply1mul  22282  coe1fzgsumdlem  22289  gsummoncoe1  22294  evl1gsumdlem  22342  mamufacex  22379  dmatelnd  22479  scmataddcl  22499  scmatsubcl  22500  scmatmulcl  22501  smatvscl  22507  mavmulsolcl  22534  mdetdiagid  22583  cramerlem3  22672  pmatcoe1fsupp  22684  cpmatacl  22699  cpmatmcllem  22701  mp2pm2mplem4  22792  chpscmat  22825  chfacfisf  22837  chfacfisfcpmat  22838  uniopn  22880  opnnei  23103  neindisj2  23106  restcls  23164  restntr  23165  tgcnp  23236  subbascn  23237  iscnp4  23246  lpcls  23347  cmpsublem  23382  cmpsub  23383  tgcmp  23384  cmpcld  23385  dfconn2  23402  1stcrest  23436  2ndcdisj  23439  1stccnp  23445  comppfsc  23515  kgencn2  23540  txlm  23631  kqreglem1  23724  filin  23837  isfil2  23839  ufilmax  23890  ufileu  23902  filufint  23903  cfinufil  23911  elfm2  23931  rnelfmlem  23935  rnelfm  23936  flimopn  23958  fbflim2  23960  flffbas  23978  fclsnei  24002  flimfnfcls  24011  fclscmp  24013  fcfnei  24018  cnpfcf  24024  alexsubALTlem2  24031  alexsubALTlem3  24032  alexsubALTlem4  24033  alexsubALT  24034  ptcmplem4  24038  qustgplem  24104  tsmsres  24127  tsmsxp  24138  metss  24491  metcnp3  24523  ovoliunnul  25492  ovolicc2lem3  25504  dyadmax  25583  itg2le  25724  bddiblnc  25827  itgcn  25830  ellimc3  25864  lhop1  25999  dvfsumrlim  26016  fta1g  26153  dvply2g  26269  fta1  26292  aalioulem3  26318  aalioulem4  26319  ulmcaulem  26377  ulmcau  26378  logbgcd1irr  26776  xrlimcnp  26950  cxploglim  26959  jensen  26970  lgsqrmodndvds  27334  gausslemma2dlem1a  27346  gausslemma2dlem2  27348  gausslemma2dlem3  27349  lgsquad2lem2  27366  2lgslem1a1  27370  2sqlem6  27404  2sq2  27414  2sqnn  27420  2sqreultblem  27429  nosepdmlem  27665  nodenselem8  27673  eqcuts3  27814  madebdaylemlrcut  27909  addsprop  27986  addsuniflem  28011  negsprop  28045  mulsprop  28140  mulsuniflem  28159  precsex  28228  onsfi  28366  elnnzs  28411  elreno2  28505  brbtwn2  28992  ax5seglem5  29020  axcontlem4  29054  axcontlem10  29060  umgrnloopv  29193  umgrnloop  29195  upgredgpr  29229  numedglnl  29231  usgrausgrb  29256  usgrnloopvALT  29288  usgrnloopALT  29290  usgredg2vlem2  29313  ushgredgedg  29316  ushgredgedgloop  29318  upgrreslem  29391  umgrreslem  29392  nbgr0edglem  29443  nbusgrvtxm1  29466  uvtxnbgrvtx  29480  cusgredg  29511  cusgrres  29535  cusgrsize2inds  29540  cusgrfi  29545  fusgrregdegfi  29656  ewlkle  29692  uspgr2wlkeqi  29734  lfgrwlkprop  29772  lfgrwlknloop  29774  pthdivtx  29813  2pthnloop  29817  upgrwlkdvdelem  29822  upgrspthswlk  29824  usgr2wlkneq  29842  usgr2trlncl  29846  usgr2pthlem  29849  usgr2pth  29850  uspgrn2crct  29894  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0  29907  wlkiswwlks1  29953  wlkiswwlks2  29961  wlkiswwlksupgr2  29963  wwlksnred  29978  wwlksnext  29979  wwlksnextbi  29980  wwlksnextwrd  29983  wwlksnextinj  29985  wwlksnextproplem2  29996  wwlksnextproplem3  29997  wspthsnonn0vne  30003  wspn0  30010  2pthon3v  30029  usgrwwlks2on  30044  umgrwwlks2on  30045  elwspths2on  30048  elwspths2onw  30049  wpthswwlks2on  30050  clwwlk1loop  30076  clwwlkccatlem  30077  umgrclwwlkge2  30079  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem3  30089  clwlkclwwlkf1lem3  30094  clwlkclwwlkfo  30097  clwwisshclwwslemlem  30101  erclwwlkeqlen  30107  erclwwlksym  30109  clwwlkf  30135  clwwlknscsh  30150  erclwwlknsym  30158  clwwlknonex2lem2  30196  clwwlknonex2  30197  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  eucrctshift  30331  3vfriswmgr  30366  1to2vfriswmgr  30367  1to3vfriswmgr  30368  n4cyclfrgr  30379  4cyclusnfrgr  30380  frgrnbnb  30381  frgrncvvdeqlem8  30394  frgrwopreg  30411  frgr2wwlk1  30417  frgr2wwlkeqm  30419  2clwwlk2clwwlklem  30434  numclwwlk1lem2fo  30446  wlkl0  30455  numclwlk2lem2f  30465  frgrreggt1  30481  frgrreg  30482  frgrregord013  30483  frgrregord13  30484  frgrogt3nreg  30485  eulplig  30574  nmoub3i  30862  ipasslem5  30924  htthlem  31006  ocin  31385  spansneleq  31659  spansnss  31660  elspansn4  31662  h1datomi  31670  nmopub2tALT  31998  nmfnleub2  32015  hstel2  32308  cvnbtwn  32375  spansncv2  32382  dmdmd  32389  dmdbr3  32394  dmdbr4  32395  dmdbr5  32397  mdsl0  32399  mdexchi  32424  cvexchlem  32457  atcv1  32469  atomli  32471  atcvatlem  32474  atcvat2i  32476  chirredi  32483  mdsymlem3  32494  mdsymlem4  32495  sumdmdii  32504  sumdmdlem  32507  cdj1i  32522  ssrelf  32707  f1o3d  32718  fisshasheq  35343  umgr2cycllem  35368  cvxpconn  35470  satfv0  35586  satfsschain  35592  satfrel  35595  satfdm  35597  satfv0fun  35599  sat1el2xp  35607  gonarlem  35622  goalrlem  35624  satffunlem1lem1  35630  satffunlem2lem1  35632  satffunlem2lem2  35634  satffun  35637  mrsubccat  35746  msubvrs  35788  fundmpss  35995  dfon2lem6  36014  dfon2lem8  36016  dfon2lem9  36017  dfon2  36018  wzel  36050  colinearxfr  36303  btwnconn1lem11  36325  lineintmo  36385  in-ax8  36452  ss-ax8  36453  trer  36544  elicc3  36545  finminlem  36546  nn0prpwlem  36550  fnessref  36585  neibastop2  36589  fgmin  36598  tailfb  36605  ordcmp  36675  ee7.2aOLD  36689  dfttc4  36758  bj-ceqsalt0  37237  bj-ceqsalt1  37238  isbasisrelowllem1  37717  isbasisrelowllem2  37718  relowlpssretop  37726  fvineqsneu  37773  fvineqsneq  37774  wl-mo3t  37947  finixpnum  37972  matunitlindflem1  37983  matunitlindflem2  37984  poimirlem26  38013  poimirlem27  38014  poimirlem29  38016  ftc1anc  38068  fdc  38112  heibor1lem  38176  ghomco  38258  rngoueqz  38307  unichnidl  38398  dmncan1  38443  ax12indn  39435  lshpdisj  39479  lub0N  39681  glb0N  39685  leat2  39786  hlrelat2  39895  cvrexchlem  39911  cvratlem  39913  atcvrj0  39920  cvrat2  39921  snatpsubN  40242  linepsubN  40244  pmaple  40253  pmapsub  40260  elpaddn0  40292  paddasslem5  40316  trlval2  40655  cdlemn11pre  41702  dihord2pre  41717  mapdordlem2  42129  sn-sup2  42981  fsuppind  43040  pell1qrgap  43319  dford3lem1  43471  hbtlem5  43573  onexlimgt  43688  onsucf1olem  43715  omcl2  43778  tfsconcat0b  43791  ntrneiiso  44535  sbiota1  44878  19.41rg  44994  ee223  45078  or2expropbilem1  47495  funressnfv  47506  fcoresf1  47532  2reuimp  47578  f1oresf1o2  47754  zm1nn  47765  nltle2tri  47776  el1fzopredsuc  47789  modlt0b  47832  mod2addne  47833  muldvdsfacgt  47849  muldvdsfacm1  47850  elsetpreimafvssdm  47861  imasetpreimafvbijlemf1  47879  iccpartlt  47899  iccpartgt  47902  iccelpart  47908  icceuelpart  47911  iccpartnel  47913  fargshiftfo  47917  fargshiftfva  47918  lswn0  47919  ich2exprop  47946  prsprel  47962  sprsymrelfolem2  47968  sprsymrelfo  47972  poprelb  47999  reuopreuprim  48001  goldbachthlem2  48024  odz2prm2pw  48041  fmtnoprmfac1  48043  fmtnofac2lem  48046  prmdvdsfmtnof1lem2  48063  2pwp1prm  48067  sfprmdvdsmersenne  48081  lighneallem3  48085  requad01  48112  requad2  48114  even3prm2  48210  fppr2odd  48222  fpprwpprb  48231  gbegt5  48252  sbgoldbwt  48268  sbgoldbalt  48272  sbgoldbm  48275  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  bgoldbtbnd  48300  tgblthelfgott  48306  tgoldbach  48308  isubgredg  48357  grimuhgr  48378  grimcnv  48379  grimco  48380  isuspgrim0  48385  isuspgrimlem  48386  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424  grimedg  48426  grtriprop  48432  cycl3grtri  48438  grimgrtri  48440  isubgr3stgrlem6  48462  uspgrlimlem3  48481  uspgrlimlem4  48482  grlimgrtrilem2  48493  grlicsym  48504  clnbgr3stgrgrlim  48510  clnbgr3stgrgrlic  48511  gpgedg2ov  48557  gpgedg2iv  48558  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  upgrwlkupwlk  48631  lmod0rng  48720  ztprmneprm  48838  ply1mulgsumlem1  48877  ply1mulgsumlem2  48878  lcoel0  48919  linindslinci  48939  lindslinindimp2lem4  48952  lindslinindsimp2lem5  48953  snlindsntor  48962  ldepspr  48964  lincresunit2  48969  fllog2  49059  dignn0ldlem  49093  dignn0flhalflem1  49106  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  itcovalt2  49168  resum2sqorgt0  49200  eenglngeehlnmlem2  49229  rrx2linest  49233  itscnhlc0xyqsol  49256  itsclc0  49262  setrec1lem2  50178  aacllem  50291