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  2249  moexexlem  2619  ralrimdvva  3184  ceqsal1t  3471  ceqsalt  3472  spcimgft  3503  vtoclgft  3509  elabgtOLD  3630  sbciegftOLD  3782  reupick  4282  reusv3  5347  sbcop1  5435  propeqop  5454  pwssun  5515  wefrc  5617  ssrel  5730  ssrel2  5732  ssrelrel  5743  ssrelrn  5841  tz7.7  6337  ordtr2  6356  onmindif  6405  unizlim  6435  funssres  6530  f1ssf1  6800  fvmptt  6954  fveqdmss  7016  fvcofneq  7031  funsndifnop  7089  funfvima2  7171  isoini  7279  isopolem  7286  weniso  7295  f1ocnv2d  7606  limsssuc  7790  tfindsg  7801  limomss  7811  findsg  7837  funcnvuni  7872  f1oweALT  7914  funelss  7989  bropopvvv  8030  bropfvvvvlem  8031  bropfvvvv  8032  f1o2ndf1  8062  frxp  8066  soseq  8099  suppfnss  8129  onfununi  8271  tz7.49  8374  omordi  8491  omlimcl  8503  omass  8505  oeordsuc  8519  nnmordi  8556  nnmord  8557  omabs  8576  xpdom2  8996  infensuc  9079  findcard2  9088  findcard2d  9090  findcard3  9187  findcard3OLD  9188  frfi  9190  xpfiOLD  9228  fsuppres  9302  dffi2  9332  elfiun  9339  ordiso2  9426  ordtypelem7  9435  suc11reg  9534  inf3lem2  9544  noinfep  9575  cantnfle  9586  cantnflem1  9604  cantnf  9608  ttrclss  9635  trcl  9643  epfrs  9646  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  10481  fpwwe2lem7  10550  tskord  10693  tskcard  10694  grupr  10710  gruiin  10723  grudomon  10730  grur1a  10732  genpn0  10916  genpcd  10919  distrlem5pr  10940  psslinpr  10944  ltaddpr  10947  ltexprlem3  10951  ltexprlem6  10954  ltapr  10958  prlem936  10960  suplem1pr  10965  axpre-sup  11082  1re  11134  dedekindle  11298  lemul12a  12000  divgt0  12011  divge0  12012  lbreu  12093  sup2  12099  bndndx  12401  elnnz  12499  nzadd  12541  fzind  12592  fnn0ind  12593  uzwo  12830  lbzbi  12855  zmax  12864  zbtwnre  12865  irradd  12892  irrmul  12893  ledivge1le  12984  xrub  13232  supxrunb2  13240  infmremnf  13264  iccid  13311  uzsubsubfz  13467  fzrevral  13533  elfz0fzfz0  13554  fz0fzelfz0  13555  elfzmlbp  13560  elincfzoext  13644  ssfzoulel  13681  ssfzo12bi  13682  fzoopth  13683  elfzonelfzo  13690  elfznelfzo  13693  elfznelfzob  13694  injresinjlem  13708  fleqceilz  13776  modaddmodup  13859  uzindi  13907  suppssfz  13919  mptnn0fsuppr  13924  le2sq2  14060  sqlecan  14134  facdiv  14212  facwordi  14214  faclbnd  14215  hashimarni  14366  hash2prd  14400  hashle2pr  14402  pr2pwpr  14404  fundmge2nop0  14427  fi1uzind  14432  brfi1indALT  14435  swrdnd2  14580  swrdnnn0nd  14581  swrdnd0  14582  pfxnd0  14613  swrdswrdlem  14628  swrdswrd  14629  ccatopth2  14641  wrd2ind  14647  pfxccatin12lem2a  14651  swrdccatin2  14653  pfxccatin12lem2  14655  pfxccatin12lem3  14656  swrdccat  14659  swrdccat3blem  14663  reuccatpfxs1lem  14670  repswswrd  14708  cshwidxmod  14727  cshwidx0  14730  2cshwcshw  14750  cshwcsh2id  14753  cau3lem  15280  caubnd  15284  climrlim2  15472  rlimcn3  15515  mulcn2  15521  climcau  15596  climbdd  15597  caucvg  15604  modfsummod  15719  p1modz1  16188  dvdsle  16239  dvdsdivcl  16245  ltoddhalfle  16290  halfleoddlt  16291  ndvdssub  16338  gcdcllem1  16428  dvdslegcd  16433  bezoutlem4  16471  dfgcd2  16475  lcmf  16562  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem  16570  lcmfdvdsb  16572  lcmfun  16574  coprmdvds1  16581  divgcdcoprm0  16594  cncongr1  16596  cncongr2  16597  prmfac1  16649  pcqcl  16786  dvdsprmpweqle  16816  oddprmdvds  16833  prmpwdvds  16834  infpnlem1  16840  prmgaplem5  16985  prmgaplem6  16986  prmgaplem7  16987  cshwshashlem1  17025  cictr  17730  initoeu2lem1  17939  initoeu2  17941  clatleglb  18442  lidrididd  18562  mulgaddcom  18995  mulginvcom  18996  cycsubm  19099  cyccom  19100  gsmsymgreqlem2  19328  symggen  19367  psgnunilem4  19394  sylow2blem3  19519  frgpnabllem1  19770  imasabl  19773  dprddisj2  19938  lmodfopnelem1  20819  lssssr  20875  lss1d  20884  lspsncv0  21071  rnglidlmcl  21141  rngqiprngimfo  21226  nzerooringczr  21405  pzriprnglem5  21410  pzriprnglem8  21413  znrrg  21490  mplcoe5lem  21962  cply1mul  22199  coe1fzgsumdlem  22206  gsummoncoe1  22211  evl1gsumdlem  22259  mamufacex  22299  dmatelnd  22399  scmataddcl  22419  scmatsubcl  22420  scmatmulcl  22421  smatvscl  22427  mavmulsolcl  22454  mdetdiagid  22503  cramerlem3  22592  pmatcoe1fsupp  22604  cpmatacl  22619  cpmatmcllem  22621  mp2pm2mplem4  22712  chpscmat  22745  chfacfisf  22757  chfacfisfcpmat  22758  uniopn  22800  opnnei  23023  neindisj2  23026  restcls  23084  restntr  23085  tgcnp  23156  subbascn  23157  iscnp4  23166  lpcls  23267  cmpsublem  23302  cmpsub  23303  tgcmp  23304  cmpcld  23305  dfconn2  23322  1stcrest  23356  2ndcdisj  23359  1stccnp  23365  comppfsc  23435  kgencn2  23460  txlm  23551  kqreglem1  23644  filin  23757  isfil2  23759  ufilmax  23810  ufileu  23822  filufint  23823  cfinufil  23831  elfm2  23851  rnelfmlem  23855  rnelfm  23856  flimopn  23878  fbflim2  23880  flffbas  23898  fclsnei  23922  flimfnfcls  23931  fclscmp  23933  fcfnei  23938  cnpfcf  23944  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  ptcmplem4  23958  qustgplem  24024  tsmsres  24047  tsmsxp  24058  metss  24412  metcnp3  24444  ovoliunnul  25424  ovolicc2lem3  25436  dyadmax  25515  itg2le  25656  bddiblnc  25759  itgcn  25762  ellimc3  25796  lhop1  25935  dvfsumrlim  25954  fta1g  26091  dvply2g  26208  fta1  26232  aalioulem3  26258  aalioulem4  26259  ulmcaulem  26319  ulmcau  26320  logbgcd1irr  26720  xrlimcnp  26894  cxploglim  26904  jensen  26915  lgsqrmodndvds  27280  gausslemma2dlem1a  27292  gausslemma2dlem2  27294  gausslemma2dlem3  27295  lgsquad2lem2  27312  2lgslem1a1  27316  2sqlem6  27350  2sq2  27360  2sqnn  27366  2sqreultblem  27375  nosepdmlem  27611  nodenselem8  27619  eqscut3  27753  madebdaylemlrcut  27831  addsprop  27906  addsuniflem  27931  negsprop  27964  mulsprop  28056  mulsuniflem  28075  precsex  28143  onsfi  28270  elnnzs  28312  brbtwn2  28868  ax5seglem5  28896  axcontlem4  28930  axcontlem10  28936  umgrnloopv  29069  umgrnloop  29071  upgredgpr  29105  numedglnl  29107  usgrausgrb  29132  usgrnloopvALT  29164  usgrnloopALT  29166  usgredg2vlem2  29189  ushgredgedg  29192  ushgredgedgloop  29194  upgrreslem  29267  umgrreslem  29268  nbgr0edglem  29319  nbusgrvtxm1  29342  uvtxnbgrvtx  29356  cusgredg  29387  cusgrres  29412  cusgrsize2inds  29417  cusgrfi  29422  fusgrregdegfi  29533  ewlkle  29569  uspgr2wlkeqi  29611  lfgrwlkprop  29649  lfgrwlknloop  29651  pthdivtx  29690  2pthnloop  29694  upgrwlkdvdelem  29699  upgrspthswlk  29701  usgr2wlkneq  29719  usgr2trlncl  29723  usgr2pthlem  29726  usgr2pth  29727  uspgrn2crct  29771  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  crctcshwlkn0  29784  wlkiswwlks1  29830  wlkiswwlks2  29838  wlkiswwlksupgr2  29840  wwlksnred  29855  wwlksnext  29856  wwlksnextbi  29857  wwlksnextwrd  29860  wwlksnextinj  29862  wwlksnextproplem2  29873  wwlksnextproplem3  29874  wspthsnonn0vne  29880  wspn0  29887  2pthon3v  29906  umgrwwlks2on  29920  elwspths2on  29923  wpthswwlks2on  29924  clwwlk1loop  29950  clwwlkccatlem  29951  umgrclwwlkge2  29953  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlklem3  29963  clwlkclwwlkf1lem3  29968  clwlkclwwlkfo  29971  clwwisshclwwslemlem  29975  erclwwlkeqlen  29981  erclwwlksym  29983  clwwlkf  30009  clwwlknscsh  30024  erclwwlknsym  30032  clwwlknonex2lem2  30070  clwwlknonex2  30071  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eucrctshift  30205  3vfriswmgr  30240  1to2vfriswmgr  30241  1to3vfriswmgr  30242  n4cyclfrgr  30253  4cyclusnfrgr  30254  frgrnbnb  30255  frgrncvvdeqlem8  30268  frgrwopreg  30285  frgr2wwlk1  30291  frgr2wwlkeqm  30293  2clwwlk2clwwlklem  30308  numclwwlk1lem2fo  30320  wlkl0  30329  numclwlk2lem2f  30339  frgrreggt1  30355  frgrreg  30356  frgrregord013  30357  frgrregord13  30358  frgrogt3nreg  30359  eulplig  30447  nmoub3i  30735  ipasslem5  30797  htthlem  30879  ocin  31258  spansneleq  31532  spansnss  31533  elspansn4  31535  h1datomi  31543  nmopub2tALT  31871  nmfnleub2  31888  hstel2  32181  cvnbtwn  32248  spansncv2  32255  dmdmd  32262  dmdbr3  32267  dmdbr4  32268  dmdbr5  32270  mdsl0  32272  mdexchi  32297  cvexchlem  32330  atcv1  32342  atomli  32344  atcvatlem  32347  atcvat2i  32349  chirredi  32356  mdsymlem3  32367  mdsymlem4  32368  sumdmdii  32377  sumdmdlem  32380  cdj1i  32395  ssrelf  32576  f1o3d  32584  fisshasheq  35090  umgr2cycllem  35115  cvxpconn  35217  satfv0  35333  satfsschain  35339  satfrel  35342  satfdm  35344  satfv0fun  35346  sat1el2xp  35354  gonarlem  35369  goalrlem  35371  satffunlem1lem1  35377  satffunlem2lem1  35379  satffunlem2lem2  35381  satffun  35384  mrsubccat  35493  msubvrs  35535  fundmpss  35742  dfon2lem6  35764  dfon2lem8  35766  dfon2lem9  35767  dfon2  35768  wzel  35800  colinearxfr  36051  btwnconn1lem11  36073  lineintmo  36133  in-ax8  36200  ss-ax8  36201  trer  36292  elicc3  36293  finminlem  36294  nn0prpwlem  36298  fnessref  36333  neibastop2  36337  fgmin  36346  tailfb  36353  ordcmp  36423  ee7.2aOLD  36437  bj-cbvalimt  36615  bj-ceqsalt0  36860  bj-ceqsalt1  36861  isbasisrelowllem1  37331  isbasisrelowllem2  37332  relowlpssretop  37340  fvineqsneu  37387  fvineqsneq  37388  wl-mo3t  37552  finixpnum  37587  matunitlindflem1  37598  matunitlindflem2  37599  poimirlem26  37628  poimirlem27  37629  poimirlem29  37631  ftc1anc  37683  fdc  37727  heibor1lem  37791  ghomco  37873  rngoueqz  37922  unichnidl  38013  dmncan1  38058  ax12indn  38924  lshpdisj  38968  lub0N  39170  glb0N  39174  leat2  39275  hlrelat2  39385  cvrexchlem  39401  cvratlem  39403  atcvrj0  39410  cvrat2  39411  snatpsubN  39732  linepsubN  39734  pmaple  39743  pmapsub  39750  elpaddn0  39782  paddasslem5  39806  trlval2  40145  cdlemn11pre  41192  dihord2pre  41207  mapdordlem2  41619  sn-sup2  42467  fsuppind  42566  pell1qrgap  42850  dford3lem1  43002  hbtlem5  43104  onexlimgt  43219  onsucf1olem  43246  omcl2  43309  tfsconcat0b  43322  ntrneiiso  44067  sbiota1  44410  19.41rg  44527  ee223  44611  or2expropbilem1  47020  funressnfv  47031  fcoresf1  47057  2reuimp  47103  f1oresf1o2  47279  zm1nn  47290  nltle2tri  47301  el1fzopredsuc  47313  modlt0b  47351  mod2addne  47352  elsetpreimafvssdm  47374  imasetpreimafvbijlemf1  47392  iccpartlt  47412  iccpartgt  47415  iccelpart  47421  icceuelpart  47424  iccpartnel  47426  fargshiftfo  47430  fargshiftfva  47431  lswn0  47432  ich2exprop  47459  prsprel  47475  sprsymrelfolem2  47481  sprsymrelfo  47485  poprelb  47512  reuopreuprim  47514  goldbachthlem2  47534  odz2prm2pw  47551  fmtnoprmfac1  47553  fmtnofac2lem  47556  prmdvdsfmtnof1lem2  47573  2pwp1prm  47577  sfprmdvdsmersenne  47591  lighneallem3  47595  requad01  47609  requad2  47611  even3prm2  47707  fppr2odd  47719  fpprwpprb  47728  gbegt5  47749  sbgoldbwt  47765  sbgoldbalt  47769  sbgoldbm  47772  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbndlem4  47796  bgoldbtbnd  47797  tgblthelfgott  47803  tgoldbach  47805  isubgredg  47854  grimuhgr  47875  grimcnv  47876  grimco  47877  isuspgrim0  47882  isuspgrimlem  47883  uhgrimisgrgriclem  47918  clnbgrgrimlem  47921  grimedg  47923  grtriprop  47929  cycl3grtri  47935  grimgrtri  47937  isubgr3stgrlem6  47959  uspgrlimlem3  47978  uspgrlimlem4  47979  grlimgrtrilem2  47990  grlicsym  48001  clnbgr3stgrgrlim  48007  clnbgr3stgrgrlic  48008  gpgedg2ov  48054  gpgedg2iv  48055  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem6  48112  upgrwlkupwlk  48128  lmod0rng  48217  ztprmneprm  48335  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  lcoel0  48417  linindslinci  48437  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  snlindsntor  48460  ldepspr  48462  lincresunit2  48467  fllog2  48557  dignn0ldlem  48591  dignn0flhalflem1  48604  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  itcovalt2  48666  resum2sqorgt0  48698  eenglngeehlnmlem2  48727  rrx2linest  48731  itscnhlc0xyqsol  48754  itsclc0  48760  setrec1lem2  49677  aacllem  49790