Theorem com23 87

Description: Commutation of antecedents. Swap 2nd and 3rd. Deduction associated with com12 33. (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 43	. 2 ⊢ (𝜒 → ((𝜒 → 𝜃) → 𝜃))
3	1, 2	syl9 78	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com3r  88  com13  89  pm2.04  91  pm2.86d  109  impcomd  417  expcomd  422  impancom  457  a2and  859  dedlem0b  1060  sbequ1  2287  moexexlem  2654  ralrimdvva  3221  ceqsal1t  3486  ceqsalt  3487  spcimgft  3514  vtoclgft  3519  elabgtOLD  3630  reupick  4277  reusv3  5374  sbcop1  5465  propeqop  5486  pwssun  5550  wefrc  5652  ssrelOLD  5768  ssrel2  5770  ssrelrel  5781  ssrelrn  5888  tz7.7  6414  ordtr2  6434  onmindif  6483  unizlim  6513  funssres  6612  f1ssf1  6888  fvmptt  7045  fveqdmss  7110  fvcofneq  7125  funsndifnop  7187  funfvima2  7268  isoini  7377  isopolem  7384  weniso  7395  f1ocnv2d  7706  limsssuc  7895  tfindsg  7906  limomss  7916  findsg  7943  funcnvuni  7978  f1oweALT  8018  funelss  8093  bropopvvv  8136  bropfvvvvlem  8137  bropfvvvv  8138  f1o2ndf1  8170  frxp  8175  soseq  8213  suppfnss  8244  onfununi  8387  tz7.48lem  8488  tz7.49  8493  omordi  8612  omlimcl  8624  omass  8626  oeordsuc  8641  nnmordi  8678  nnmord  8679  omabs  8698  xpdom2  9129  infensuc  9212  findcard2  9218  findcard2d  9220  findcard3  9312  frfi  9314  fsuppres  9422  dffi2  9452  elfiun  9459  ordiso2  9546  ordtypelem7  9555  suc11reg  9657  inf3lem2  9667  noinfep  9698  cantnfle  9709  cantnflem1  9727  cantnf  9731  ttrclss  9758  trcl  9766  epfrs  9769  frr3g  9797  r1sdom  9818  setrec1lem2  10004  updjud  10052  dfac8alem  10147  indcardi  10159  alephordi  10192  dfac12lem3  10263  pwsdompw  10320  cofsmo  10386  cfcoflem  10389  coftr  10390  isf32lem2  10471  isf32lem9  10478  axcc3  10555  domtriomlem  10559  axdc3lem2  10568  axdc3lem4  10570  zorn2lem4  10616  zorn2lem6  10618  zorn2lem7  10619  ttukeylem6  10631  uniimadom  10667  konigthlem  10692  fpwwe2lem7  10761  tskord  10904  tskcard  10905  grupr  10921  gruiin  10934  grudomon  10941  grur1a  10943  genpn0  11127  genpcd  11130  distrlem5pr  11151  psslinpr  11155  ltaddpr  11158  ltexprlem3  11162  ltexprlem6  11165  ltapr  11169  prlem936  11171  suplem1pr  11176  axpre-sup  11293  1re  11347  dedekindle  11513  lemul12a  12215  divgt0  12225  divge0  12226  lbreu  12307  sup2  12313  bndndx  12645  elnnz  12743  nzadd  12784  fzind  12837  fnn0ind  12838  uzwo  13078  lbzbi  13103  zmax  13112  zbtwnre  13113  irradd  13141  irrmul  13142  ledivge1le  13233  xrub  13482  supxrunb2  13490  infmremnf  13514  iccid  13561  uzsubsubfz  13720  fzrevral  13786  elfz0fzfz0  13807  fz0fzelfz0  13808  elfzmlbp  13813  elincfzoext  13898  ssfzoulel  13935  ssfzo12bi  13936  fzoopth  13937  elfzonelfzo  13944  elfznelfzo  13948  elfznelfzob  13949  injresinjlem  13965  fleqceilz  14034  modaddmodup  14117  uzindi  14165  suppssfz  14177  mptnn0fsuppr  14182  le2sq2  14318  sqlecan  14393  facdiv  14472  facwordi  14474  faclbnd  14475  hashimarni  14627  hash2prd  14661  hashle2pr  14663  pr2pwpr  14665  fundmge2nop0  14688  fi1uzind  14693  brfi1indALT  14696  swrdnd2  14847  swrdnnn0nd  14848  swrdnd0  14849  pfxnd0  14880  swrdswrdlem  14895  swrdswrd  14896  ccatopth2  14908  wrd2ind  14914  pfxccatin12lem2a  14918  swrdccatin2  14920  pfxccatin12lem2  14922  pfxccatin12lem3  14923  swrdccat  14926  swrdccat3blem  14930  reuccatpfxs1lem  14937  repswswrd  14977  cshwidxmod  14996  cshwidx0  14999  2cshwcshw  15018  cshwcsh2id  15021  cau3lem  15566  caubnd  15570  climrlim2  15758  rlimcn3  15801  mulcn2  15807  climcau  15882  climbdd  15883  caucvg  15890  modfsummod  16005  p1modz1  16473  dvdsle  16524  dvdsdivcl  16530  ltoddhalfle  16575  halfleoddlt  16576  ndvdssub  16623  gcdcllem1  16713  dvdslegcd  16718  bezoutlem4  16759  dfgcd2  16763  lcmf  16852  lcmfunsnlem1  16856  lcmfunsnlem2lem1  16857  lcmfunsnlem  16860  lcmfdvdsb  16862  lcmfun  16864  coprmdvds1  16871  divgcdcoprm0  16884  cncongr1  16886  cncongr2  16887  prmfac1  16940  pcqcl  17078  dvdsprmpweqle  17108  oddprmdvds  17125  prmpwdvds  17126  infpnlem1  17132  prmgaplem5  17277  prmgaplem6  17278  prmgaplem7  17279  cshwshashlem1  17317  cictr  18030  initoeu2lem1  18239  initoeu2  18241  clatleglb  18742  lidrididd  18901  mulgaddcom  19358  mulginvcom  19359  cycsubm  19467  cyccom  19468  gsmsymgreqlem2  19696  symggen  19735  psgnunilem4  19762  sylow2blem3  19887  frgpnabllem1  20138  imasabl  20141  dprddisj2  20306  lmodfopnelem1  21224  lssssr  21280  lss1d  21289  lspsncv0  21475  rnglidlmcl  21546  lidlunin0  21566  unichnlidl  21567  rngqiprngimfo  21648  nzerooringczr  21841  pzriprnglem5  21846  pzriprnglem8  21849  znrrg  21926  mplcoe5lem  22403  cply1mul  22669  coe1fzgsumdlem  22676  gsummoncoe1  22681  evl1gsumdlem  22729  mamufacex  22766  dmatelnd  22866  scmataddcl  22886  scmatsubcl  22887  scmatmulcl  22888  smatvscl  22894  mavmulsolcl  22921  mdetdiagid  22970  matunitlindflem1  23049  matunitlindflem2  23050  cramerlem3  23062  pmatcoe1fsupp  23074  cpmatacl  23089  cpmatmcllem  23091  mp2pm2mplem4  23182  chpscmat  23215  chfacfisf  23227  chfacfisfcpmat  23228  uniopn  23270  opnnei  23493  neindisj2  23496  restcls  23554  restntr  23555  tgcnp  23626  subbascn  23627  iscnp4  23636  lpcls  23737  cmpsublem  23772  cmpsub  23773  tgcmp  23774  cmpcld  23775  dfconn2  23792  1stcrest  23826  2ndcdisj  23830  1stccnp  23836  comppfsc  23906  kgencn2  23931  txlm  24022  kqreglem1  24115  filin  24228  isfil2  24230  ufilmax  24281  ufileu  24293  filufint  24294  cfinufil  24302  elfm2  24322  rnelfmlem  24326  rnelfm  24327  flimopn  24349  fbflim2  24351  flffbas  24369  fclsnei  24393  flimfnfcls  24402  fclscmp  24404  fcfnei  24409  cnpfcf  24415  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALTlem4  24424  alexsubALT  24425  ptcmplem4  24429  qustgplem  24495  tsmsres  24518  tsmsxp  24529  metss  24882  metcnp3  24914  ovoliunnul  25883  ovolicc2lem3  25895  dyadmax  25974  itg2le  26115  bddiblnc  26217  itgcn  26220  ellimc3  26254  lhop1  26389  dvfsumrlim  26406  fta1g  26543  dvply2g  26661  fta1  26684  aalioulem3  26718  aalioulem4  26719  ulmcaulem  26778  ulmcau  26779  logbgcd1irr  27179  xrlimcnp  27353  cxploglim  27362  jensen  27373  lgsqrmodndvds  27737  gausslemma2dlem1a  27749  gausslemma2dlem2  27751  gausslemma2dlem3  27752  lgsquad2lem2  27769  2lgslem1a1  27773  2sqlem6  27807  2sq2  27817  2sqnn  27823  2sqreultblem  27832  fltoprm  28052  fltoprmgt3  28053  nosepdmlem  28097  nodenselem8  28105  eqcuts3  28247  madebdaylemlrcut  28342  addsprop  28419  addsuniflem  28444  negsprop  28478  mulsprop  28573  mulsuniflem  28592  precsex  28661  onsfi  28799  elnnzs  28844  elreno2  28938  brbtwn2  29540  ax5seglem5  29568  axcontlem4  29602  axcontlem10  29608  umgrnloopv  29741  umgrnloop  29743  upgredgpr  29777  numedglnl  29779  usgrausgrb  29807  usgrnloopvALT  29839  usgrnloopALT  29841  usgredg2vlem2  29864  ushgredgedg  29867  ushgredgedgloop  29869  upgrreslem  29942  umgrreslem  29943  nbgr0edglem  29994  nbusgrvtxm1  30017  uvtxnbgrvtx  30031  cusgredg  30062  cusgrres  30086  cusgrsize2inds  30091  cusgrfi  30096  fusgrregdegfi  30207  ewlkle  30243  uspgr2wlkeqi  30285  lfgrwlkprop  30327  lfgrwlknloop  30329  pthdivtx  30369  2pthnloop  30374  upgrwlkdvdelem  30379  upgrspthswlk  30381  usgr2wlkneq  30399  usgr2trlncl  30403  usgr2pthlem  30406  usgr2pth  30407  uspgrn2crct  30454  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  crctcshwlkn0  30467  wlkiswwlks1  30513  wlkiswwlks2  30521  wlkiswwlksupgr2  30523  wwlksnred  30538  wwlksnext  30539  wwlksnextbi  30540  wwlksnextwrd  30543  wwlksnextinj  30545  wwlksnextproplem2  30556  wwlksnextproplem3  30557  wspthsnonn0vne  30563  wspn0  30570  2pthon3v  30589  usgrwwlks2on  30604  umgrwwlks2on  30605  elwspths2on  30608  elwspths2onw  30609  wpthswwlks2on  30610  clwwlk1loop  30636  clwwlkccatlem  30637  umgrclwwlkge2  30639  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwlkclwwlklem3  30649  clwlkclwwlkf1lem3  30654  clwlkclwwlkfo  30657  clwwisshclwwslemlem  30661  erclwwlkeqlen  30667  erclwwlksym  30669  clwwlkf  30695  clwwlknscsh  30710  erclwwlknsym  30718  clwwlknonex2lem2  30756  clwwlknonex2  30757  umgr2cycllem  30803  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  eucrctshift  30901  3vfriswmgr  30936  1to2vfriswmgr  30937  1to3vfriswmgr  30938  n4cyclfrgr  30949  4cyclusnfrgr  30950  frgrnbnb  30951  frgrncvvdeqlem8  30964  frgrwopreg  30981  frgr2wwlk1  30987  frgr2wwlkeqm  30989  2clwwlk2clwwlklem  31004  numclwwlk1lem2fo  31016  wlkl0  31025  numclwlk2lem2f  31035  frgrreggt1  31051  frgrreg  31052  frgrregord013  31053  frgrregord13  31054  frgrogt3nreg  31055  eulplig  31144  nmoub3i  31432  ipasslem5  31494  htthlem  31576  ocin  31955  spansneleq  32229  spansnss  32230  elspansn4  32232  h1datomi  32240  nmopub2tALT  32568  nmfnleub2  32585  hstel2  32878  cvnbtwn  32945  spansncv2  32952  dmdmd  32959  dmdbr3  32964  dmdbr4  32965  dmdbr5  32967  mdsl0  32969  mdexchi  32994  cvexchlem  33027  atcv1  33039  atomli  33041  atcvatlem  33044  atcvat2i  33046  chirredi  33053  mdsymlem3  33064  mdsymlem4  33065  sumdmdii  33074  sumdmdlem  33077  cdj1i  33092  ssrelf  33307  f1o3d  33318  onprcf1acwevdlem1  36086  fisshasheq  36101  cvxpconn  36215  satfv0  36331  satfsschain  36337  satfrel  36340  satfdm  36342  satfv0fun  36344  sat1el2xp  36352  gonarlem  36367  goalrlem  36369  satffunlem1lem1  36375  satffunlem2lem1  36377  satffunlem2lem2  36379  satffun  36382  mrsubccat  36491  msubvrs  36533  mirimanofffr  36670  elpssmo  36673  fundmpss  36747  dfon2lem6  36765  dfon2lem8  36767  dfon2lem9  36768  dfon2  36769  wzel  36801  colinearxfr  37055  btwnconn1lem11  37077  lineintmo  37137  in-ax8  37228  ss-ax8  37229  trer  37319  elicc3  37320  finminlem  37321  nn0prpwlem  37325  fnessref  37360  neibastop2  37364  fgmin  37373  tailfb  37380  ordcmp  37450  ee7.2aOLD  37464  dfttc4  37533  bj-ceqsalt0  38011  bj-ceqsalt1  38012  isbasisrelowllem1  38546  isbasisrelowllem2  38547  relowlpssretop  38555  fvineqsneu  38602  fvineqsneq  38603  wl-mo3t  38776  finixpnum  38796  poimirlem26  38832  poimirlem27  38833  poimirlem29  38835  ftc1anc  38887  fdc  38945  heibor1lem  39009  ghomco  39091  rngoueqz  39140  unichnidl  39231  dmncan1  39276  ax12indn  40266  lshpdisj  40310  lub0N  40512  glb0N  40516  leat2  40617  hlrelat2  40726  cvrexchlem  40742  cvratlem  40744  atcvrj0  40751  cvrat2  40752  snatpsubN  41073  linepsubN  41075  pmaple  41084  pmapsub  41091  elpaddn0  41123  paddasslem5  41147  trlval2  41486  cdlemn11pre  42533  dihord2pre  42548  mapdordlem2  42960  sn-sup2  43821  fsuppind  43884  pell1qrgap  44147  dford3lem1  44299  hbtlem5  44395  onexlimgt  44506  onsucf1olem  44533  omcl2  44596  tfsconcat0b  44609  ntrneiiso  45352  sbiota1  45678  19.41rg  45793  ee223  45877  cocanss2  46183  or2expropbilem1  48375  funressnfv  48386  fcoresf1  48412  aiotaexim  48441  2reuimp  48459  f1oresf1o2  48634  zm1nn  48645  nltle2tri  48656  el1fzopredsuc  48669  modlt0b  48712  mod2addne  48713  muldvdsfacgt  48729  muldvdsfacm1  48730  elsetpreimafvssdm  48741  imasetpreimafvbijlemf1  48759  iccpartlt  48779  iccpartgt  48782  iccelpart  48788  icceuelpart  48791  iccpartnel  48793  fargshiftfo  48797  fargshiftfva  48798  lswn0  48799  ich2exprop  48826  prsprel  48842  sprsymrelfolem2  48848  sprsymrelfo  48852  poprelb  48879  reuopreuprim  48881  goldbachthlem2  48904  odz2prm2pw  48921  fmtnoprmfac1  48923  fmtnofac2lem  48926  prmdvdsfmtnof1lem2  48943  2pwp1prm  48947  sfprmdvdsmersenne  48961  lighneallem3  48965  requad01  48992  requad2  48994  even3prm2  49090  fppr2odd  49102  fpprwpprb  49111  gbegt5  49132  sbgoldbwt  49148  sbgoldbalt  49152  sbgoldbm  49155  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbndlem4  49179  bgoldbtbnd  49180  tgblthelfgott  49186  tgoldbach  49188  isubgredg  49237  grimuhgr  49258  grimcnv  49259  grimco  49260  isuspgrim0  49265  isuspgrimlem  49266  uhgrimisgrgriclem  49301  clnbgrgrimlem  49304  grimedg  49306  grtriprop  49312  cycl3grtri  49318  grimgrtri  49320  isubgr3stgrlem6  49342  uspgrlimlem3  49361  uspgrlimlem4  49362  grlimgrtrilem2  49373  grlicsym  49384  clnbgr3stgrgrlim  49390  clnbgr3stgrgrlic  49391  gpgedg2ov  49437  gpgedg2iv  49438  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem6  49495  upgrwlkupwlk  49511  lmod0rng  49599  lazaddcl  49738  lazmulcl  49740  idomcanl  49775  ztprmneprm  49790  ply1mulgsumlem1  49829  ply1mulgsumlem2  49830  lcoel0  49871  linindslinci  49891  lindslinindimp2lem4  49904  lindslinindsimp2lem5  49905  snlindsntor  49914  ldepspr  49916  lincresunit2  49921  fllog2  50011  dignn0ldlem  50045  dignn0flhalflem1  50058  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  itcovalt2  50120  resum2sqorgt0  50152  eenglngeehlnmlem2  50182  rrx2linest  50185  itscnhlc0xyqsol  50208  itsclc0  50214  aacllem  51367