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  842  dedlem0b  1042  sbequ1  2239  moexexlem  2621  ralrimdvva  3208  ceqsal1t  3504  ceqsalt  3505  vtoclgft  3540  sbciegft  3815  reupick  4318  reusv3  5403  sbcop1  5488  propeqop  5507  pwssun  5571  wefrc  5670  ssrel  5782  ssrelOLD  5783  ssrel2  5785  ssrelrel  5796  ssrelrn  5894  tz7.7  6390  ordtr2  6408  onmindif  6456  unizlim  6487  funssres  6592  f1ssf1  6865  fvmptt  7018  fveqdmss  7080  fvcofneq  7094  funsndifnop  7151  funfvima2  7235  isoini  7338  isopolem  7345  weniso  7354  f1ocnv2d  7663  limsssuc  7843  tfindsg  7854  limomss  7864  findsg  7894  funcnvuni  7926  f1oweALT  7963  funelss  8037  bropopvvv  8081  bropfvvvvlem  8082  bropfvvvv  8083  f1o2ndf1  8113  frxp  8117  soseq  8150  suppfnss  8179  wfrlem12OLD  8326  onfununi  8347  tz7.49  8451  omordi  8572  omlimcl  8584  omass  8586  oeordsuc  8600  nnmordi  8637  nnmord  8638  omabs  8656  xpdom2  9073  infensuc  9161  findcard2  9170  findcard2d  9172  findcard2OLD  9290  findcard3  9291  findcard3OLD  9292  frfi  9294  xpfiOLD  9324  fsuppres  9394  dffi2  9424  elfiun  9431  ordiso2  9516  ordtypelem7  9525  suc11reg  9620  inf3lem2  9630  noinfep  9661  cantnfle  9672  cantnflem1  9690  cantnf  9694  ttrclss  9721  trcl  9729  epfrs  9732  frr3g  9757  r1sdom  9775  updjud  9935  pr2neOLD  10006  dfac8alem  10030  indcardi  10042  alephordi  10075  dfac12lem3  10146  pwsdompw  10205  cofsmo  10270  cfcoflem  10273  coftr  10274  isf32lem2  10355  isf32lem9  10362  axcc3  10439  domtriomlem  10443  axdc3lem2  10452  axdc3lem4  10454  zorn2lem4  10500  zorn2lem6  10502  zorn2lem7  10503  ttukeylem6  10515  uniimadom  10545  konigthlem  10569  fpwwe2lem7  10638  tskord  10781  tskcard  10782  grupr  10798  gruiin  10811  grudomon  10818  grur1a  10820  genpn0  11004  genpcd  11007  distrlem5pr  11028  psslinpr  11032  ltaddpr  11035  ltexprlem3  11039  ltexprlem6  11042  ltapr  11046  prlem936  11048  suplem1pr  11053  axpre-sup  11170  1re  11221  dedekindle  11385  lemul12a  12079  divgt0  12089  divge0  12090  lbreu  12171  sup2  12177  bndndx  12478  elnnz  12575  nzadd  12617  fzind  12667  fnn0ind  12668  uzwo  12902  lbzbi  12927  zmax  12936  zbtwnre  12937  irradd  12964  irrmul  12965  ledivge1le  13052  xrub  13298  supxrunb2  13306  infmremnf  13329  iccid  13376  uzsubsubfz  13530  fzrevral  13593  elfz0fzfz0  13613  fz0fzelfz0  13614  elfzmlbp  13619  elincfzoext  13697  ssfzoulel  13733  ssfzo12bi  13734  elfzonelfzo  13741  elfznelfzo  13744  elfznelfzob  13745  injresinjlem  13759  fleqceilz  13826  modaddmodup  13906  uzindi  13954  suppssfz  13966  mptnn0fsuppr  13971  le2sq2  14107  sqlecan  14180  facdiv  14254  facwordi  14256  faclbnd  14257  hashimarni  14408  hash2prd  14443  hashle2pr  14445  pr2pwpr  14447  fundmge2nop0  14460  fi1uzind  14465  brfi1indALT  14468  swrdnd2  14612  swrdnnn0nd  14613  swrdnd0  14614  pfxnd0  14645  swrdswrdlem  14661  swrdswrd  14662  ccatopth2  14674  wrd2ind  14680  pfxccatin12lem2a  14684  swrdccatin2  14686  pfxccatin12lem2  14688  pfxccatin12lem3  14689  swrdccat  14692  swrdccat3blem  14696  reuccatpfxs1lem  14703  repswswrd  14741  cshwidxmod  14760  cshwidx0  14763  2cshwcshw  14783  cshwcsh2id  14786  cau3lem  15308  caubnd  15312  climrlim2  15498  rlimcn3  15541  mulcn2  15547  climcau  15624  climbdd  15625  caucvg  15632  modfsummod  15747  p1modz1  16211  dvdsle  16260  dvdsdivcl  16266  ltoddhalfle  16311  halfleoddlt  16312  ndvdssub  16359  gcdcllem1  16447  dvdslegcd  16452  bezoutlem4  16491  dfgcd2  16495  lcmf  16577  lcmfunsnlem1  16581  lcmfunsnlem2lem1  16582  lcmfunsnlem  16585  lcmfdvdsb  16587  lcmfun  16589  coprmdvds1  16596  divgcdcoprm0  16609  cncongr1  16611  cncongr2  16612  prmfac1  16665  pcqcl  16796  dvdsprmpweqle  16826  oddprmdvds  16843  prmpwdvds  16844  infpnlem1  16850  prmgaplem5  16995  prmgaplem6  16996  prmgaplem7  16997  cshwshashlem1  17036  cictr  17759  initoeu2lem1  17974  initoeu2  17976  clatleglb  18481  lidrididd  18601  mulgaddcom  19021  mulginvcom  19022  cycsubm  19124  cyccom  19125  gsmsymgreqlem2  19347  symggen  19386  psgnunilem4  19413  sylow2blem3  19538  frgpnabllem1  19789  imasabl  19792  dprddisj2  19957  lmodfopnelem1  20740  lssssr  20797  lss1d  20806  lspsncv0  20993  rnglidlmcl  21071  rngqiprngimfo  21149  nzerooringczr  21340  pzriprnglem5  21345  pzriprnglem8  21348  znrrg  21431  mplcoe5lem  21905  cply1mul  22138  coe1fzgsumdlem  22145  gsummoncoe1  22148  evl1gsumdlem  22195  mamufacex  22211  dmatelnd  22318  scmataddcl  22338  scmatsubcl  22339  scmatmulcl  22340  smatvscl  22346  mavmulsolcl  22373  mdetdiagid  22422  cramerlem3  22511  pmatcoe1fsupp  22523  cpmatacl  22538  cpmatmcllem  22540  mp2pm2mplem4  22631  chpscmat  22664  chfacfisf  22676  chfacfisfcpmat  22677  uniopn  22719  opnnei  22944  neindisj2  22947  restcls  23005  restntr  23006  tgcnp  23077  subbascn  23078  iscnp4  23087  lpcls  23188  cmpsublem  23223  cmpsub  23224  tgcmp  23225  cmpcld  23226  dfconn2  23243  1stcrest  23277  2ndcdisj  23280  1stccnp  23286  comppfsc  23356  kgencn2  23381  txlm  23472  kqreglem1  23565  filin  23678  isfil2  23680  ufilmax  23731  ufileu  23743  filufint  23744  cfinufil  23752  elfm2  23772  rnelfmlem  23776  rnelfm  23777  flimopn  23799  fbflim2  23801  flffbas  23819  fclsnei  23843  flimfnfcls  23852  fclscmp  23854  fcfnei  23859  cnpfcf  23865  alexsubALTlem2  23872  alexsubALTlem3  23873  alexsubALTlem4  23874  alexsubALT  23875  ptcmplem4  23879  qustgplem  23945  tsmsres  23968  tsmsxp  23979  metss  24337  metcnp3  24369  ovoliunnul  25356  ovolicc2lem3  25368  dyadmax  25447  itg2le  25589  bddiblnc  25691  itgcn  25694  ellimc3  25728  lhop1  25867  dvfsumrlim  25886  fta1g  26023  fta1  26160  aalioulem3  26186  aalioulem4  26187  ulmcaulem  26245  ulmcau  26246  logbgcd1irr  26640  xrlimcnp  26814  cxploglim  26823  jensen  26834  lgsqrmodndvds  27199  gausslemma2dlem1a  27211  gausslemma2dlem2  27213  gausslemma2dlem3  27214  lgsquad2lem2  27231  2lgslem1a1  27235  2sqlem6  27269  2sq2  27279  2sqnn  27285  2sqreultblem  27294  nosepdmlem  27529  nodenselem8  27537  madebdaylemlrcut  27738  addsprop  27806  addsuniflem  27831  negsprop  27860  mulsprop  27943  mulsuniflem  27962  precsex  28029  brbtwn2  28596  ax5seglem5  28624  axcontlem4  28658  axcontlem10  28664  umgrnloopv  28799  umgrnloop  28801  upgredgpr  28835  numedglnl  28837  usgrausgrb  28862  usgrnloopvALT  28891  usgrnloopALT  28893  usgredg2vlem2  28916  ushgredgedg  28919  ushgredgedgloop  28921  upgrreslem  28994  umgrreslem  28995  nbgr0vtxlem  29045  nbusgrvtxm1  29069  uvtxnbgrvtx  29083  cusgredg  29114  cusgrres  29138  cusgrsize2inds  29143  cusgrfi  29148  fusgrregdegfi  29259  ewlkle  29295  uspgr2wlkeqi  29338  lfgrwlkprop  29377  lfgrwlknloop  29379  pthdivtx  29419  2pthnloop  29421  upgrwlkdvdelem  29426  upgrspthswlk  29428  usgr2wlkneq  29446  usgr2trlncl  29450  usgr2pthlem  29453  usgr2pth  29454  uspgrn2crct  29495  crctcshwlkn0lem4  29500  crctcshwlkn0lem5  29501  crctcshwlkn0  29508  wlkiswwlks1  29554  wlkiswwlks2  29562  wlkiswwlksupgr2  29564  wwlksnred  29579  wwlksnext  29580  wwlksnextbi  29581  wwlksnextwrd  29584  wwlksnextinj  29586  wwlksnextproplem2  29597  wwlksnextproplem3  29598  wspthsnonn0vne  29604  wspn0  29611  2pthon3v  29630  umgrwwlks2on  29644  elwspths2on  29647  wpthswwlks2on  29648  clwwlk1loop  29674  clwwlkccatlem  29675  umgrclwwlkge2  29677  clwlkclwwlklem2a4  29683  clwlkclwwlklem2a  29684  clwlkclwwlklem3  29687  clwlkclwwlkf1lem3  29692  clwlkclwwlkfo  29695  clwwisshclwwslemlem  29699  erclwwlkeqlen  29705  erclwwlksym  29707  clwwlkf  29733  clwwlknscsh  29748  erclwwlknsym  29756  clwwlknonex2lem2  29794  clwwlknonex2  29795  upgr3v3e3cycl  29866  upgr4cycl4dv4e  29871  eucrctshift  29929  3vfriswmgr  29964  1to2vfriswmgr  29965  1to3vfriswmgr  29966  n4cyclfrgr  29977  4cyclusnfrgr  29978  frgrnbnb  29979  frgrncvvdeqlem8  29992  frgrwopreg  30009  frgr2wwlk1  30015  frgr2wwlkeqm  30017  2clwwlk2clwwlklem  30032  numclwwlk1lem2fo  30044  wlkl0  30053  numclwlk2lem2f  30063  frgrreggt1  30079  frgrreg  30080  frgrregord013  30081  frgrregord13  30082  frgrogt3nreg  30083  eulplig  30171  nmoub3i  30459  ipasslem5  30521  htthlem  30603  ocin  30982  spansneleq  31256  spansnss  31257  elspansn4  31259  h1datomi  31267  nmopub2tALT  31595  nmfnleub2  31612  hstel2  31905  cvnbtwn  31972  spansncv2  31979  dmdmd  31986  dmdbr3  31991  dmdbr4  31992  dmdbr5  31994  mdsl0  31996  mdexchi  32021  cvexchlem  32054  atcv1  32066  atomli  32068  atcvatlem  32071  atcvat2i  32073  chirredi  32080  mdsymlem3  32091  mdsymlem4  32092  sumdmdii  32101  sumdmdlem  32104  cdj1i  32119  ssrelf  32277  f1o3d  32284  fisshasheq  34568  umgr2cycllem  34595  cvxpconn  34697  satfv0  34813  satfsschain  34819  satfrel  34822  satfdm  34824  satfv0fun  34826  sat1el2xp  34834  gonarlem  34849  goalrlem  34851  satffunlem1lem1  34857  satffunlem2lem1  34859  satffunlem2lem2  34861  satffun  34864  mrsubccat  34973  msubvrs  35015  fundmpss  35208  dfon2lem6  35230  dfon2lem8  35232  dfon2lem9  35233  dfon2  35234  wzel  35266  colinearxfr  35517  btwnconn1lem11  35539  lineintmo  35599  trer  35665  elicc3  35666  finminlem  35667  nn0prpwlem  35671  fnessref  35706  neibastop2  35710  fgmin  35719  tailfb  35726  ordcmp  35796  ee7.2aOLD  35810  bj-cbvalimt  35980  bj-ceqsalt0  36228  bj-ceqsalt1  36229  isbasisrelowllem1  36700  isbasisrelowllem2  36701  relowlpssretop  36709  fvineqsneu  36756  fvineqsneq  36757  wl-mo3t  36905  finixpnum  36937  matunitlindflem1  36948  matunitlindflem2  36949  poimirlem26  36978  poimirlem27  36979  poimirlem29  36981  ftc1anc  37033  fdc  37077  heibor1lem  37141  ghomco  37223  rngoueqz  37272  unichnidl  37363  dmncan1  37408  ax12indn  38277  lshpdisj  38321  lub0N  38523  glb0N  38527  leat2  38628  hlrelat2  38738  cvrexchlem  38754  cvratlem  38756  atcvrj0  38763  cvrat2  38764  snatpsubN  39085  linepsubN  39087  pmaple  39096  pmapsub  39103  elpaddn0  39135  paddasslem5  39159  trlval2  39498  cdlemn11pre  40545  dihord2pre  40560  mapdordlem2  40972  fsuppind  41625  sn-sup2  41805  pell1qrgap  42075  dford3lem1  42228  hbtlem5  42333  onexlimgt  42455  onsucf1olem  42483  omcl2  42546  tfsconcat0b  42559  ntrneiiso  43305  sbiota1  43656  19.41rg  43774  ee223  43858  or2expropbilem1  46201  funressnfv  46212  fcoresf1  46238  2reuimp  46282  f1oresf1o2  46458  zm1nn  46469  nltle2tri  46480  el1fzopredsuc  46492  fzoopth  46494  elsetpreimafvssdm  46513  imasetpreimafvbijlemf1  46531  iccpartlt  46551  iccpartgt  46554  iccelpart  46560  icceuelpart  46563  iccpartnel  46565  fargshiftfo  46569  fargshiftfva  46570  lswn0  46571  ich2exprop  46598  prsprel  46614  sprsymrelfolem2  46620  sprsymrelfo  46624  poprelb  46651  reuopreuprim  46653  goldbachthlem2  46673  odz2prm2pw  46690  fmtnoprmfac1  46692  fmtnofac2lem  46695  prmdvdsfmtnof1lem2  46712  2pwp1prm  46716  sfprmdvdsmersenne  46730  lighneallem3  46734  requad01  46748  requad2  46750  even3prm2  46846  fppr2odd  46858  fpprwpprb  46867  gbegt5  46888  sbgoldbwt  46904  sbgoldbalt  46908  sbgoldbm  46911  bgoldbtbndlem2  46933  bgoldbtbndlem3  46934  bgoldbtbndlem4  46935  bgoldbtbnd  46936  tgblthelfgott  46942  tgoldbach  46944  isomuspgrlem2b  46956  isomuspgrlem2d  46958  isomuspgr  46961  isomgrsym  46963  upgrwlkupwlk  46977  lmod0rng  47066  ztprmneprm  47186  ply1mulgsumlem1  47229  ply1mulgsumlem2  47230  lcoel0  47271  linindslinci  47291  lindslinindimp2lem4  47304  lindslinindsimp2lem5  47305  snlindsntor  47314  ldepspr  47316  lincresunit2  47321  fllog2  47416  dignn0ldlem  47450  dignn0flhalflem1  47463  nn0sumshdiglemA  47467  nn0sumshdiglemB  47468  itcovalt2  47525  resum2sqorgt0  47557  eenglngeehlnmlem2  47586  rrx2linest  47590  itscnhlc0xyqsol  47613  itsclc0  47619  setrec1lem2  47895  aacllem  48010