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  415  expcomd  420  impancom  455  a2and  856  dedlem0b  1055  sbequ1  2282  moexexlem  2652  ralrimdvva  3216  ceqsal1t  3485  ceqsalt  3486  spcimgft  3513  vtoclgft  3519  elabgtOLD  3631  reupick  4279  reusv3  5359  sbcop1  5453  propeqop  5473  pwssun  5535  wefrc  5637  ssrel  5751  ssrel2  5753  ssrelrel  5764  ssrelrn  5866  tz7.7  6367  ordtr2  6386  onmindif  6435  unizlim  6465  funssres  6560  f1ssf1  6834  fvmptt  6991  fveqdmss  7054  fvcofneq  7069  funsndifnop  7129  funfvima2  7210  isoini  7317  isopolem  7324  weniso  7333  f1ocnv2d  7644  limsssuc  7825  tfindsg  7836  limomss  7846  findsg  7873  funcnvuni  7908  f1oweALT  7948  funelss  8023  bropopvvv  8063  bropfvvvvlem  8064  bropfvvvv  8065  f1o2ndf1  8095  frxp  8100  soseq  8133  suppfnss  8163  onfununi  8306  tz7.49  8410  omordi  8529  omlimcl  8541  omass  8543  oeordsuc  8558  nnmordi  8595  nnmord  8596  omabs  8615  xpdom2  9038  infensuc  9121  findcard2  9127  findcard2d  9129  findcard3  9221  frfi  9223  fsuppres  9333  dffi2  9363  elfiun  9370  ordiso2  9457  ordtypelem7  9466  suc11reg  9568  inf3lem2  9578  noinfep  9609  cantnfle  9620  cantnflem1  9638  cantnf  9642  ttrclss  9669  trcl  9677  epfrs  9680  frr3g  9708  r1sdom  9726  updjud  9886  dfac8alem  9979  indcardi  9991  alephordi  10024  dfac12lem3  10096  pwsdompw  10153  cofsmo  10220  cfcoflem  10223  coftr  10224  isf32lem2  10305  isf32lem9  10312  axcc3  10389  domtriomlem  10393  axdc3lem2  10402  axdc3lem4  10404  zorn2lem4  10450  zorn2lem6  10452  zorn2lem7  10453  ttukeylem6  10465  uniimadom  10495  konigthlem  10520  fpwwe2lem7  10589  tskord  10732  tskcard  10733  grupr  10749  gruiin  10762  grudomon  10769  grur1a  10771  genpn0  10955  genpcd  10958  distrlem5pr  10979  psslinpr  10983  ltaddpr  10986  ltexprlem3  10990  ltexprlem6  10993  ltapr  10997  prlem936  10999  suplem1pr  11004  axpre-sup  11121  1re  11175  dedekindle  11341  lemul12a  12043  divgt0  12054  divge0  12055  lbreu  12136  sup2  12142  bndndx  12474  elnnz  12572  nzadd  12613  fzind  12665  fnn0ind  12666  uzwo  12906  lbzbi  12931  zmax  12940  zbtwnre  12941  irradd  12968  irrmul  12969  ledivge1le  13060  xrub  13309  supxrunb2  13317  infmremnf  13341  iccid  13388  uzsubsubfz  13545  fzrevral  13611  elfz0fzfz0  13632  fz0fzelfz0  13633  elfzmlbp  13638  elincfzoext  13723  ssfzoulel  13760  ssfzo12bi  13761  fzoopth  13762  elfzonelfzo  13769  elfznelfzo  13773  elfznelfzob  13774  injresinjlem  13790  fleqceilz  13858  modaddmodup  13941  uzindi  13989  suppssfz  14001  mptnn0fsuppr  14006  le2sq2  14142  sqlecan  14216  facdiv  14294  facwordi  14296  faclbnd  14297  hashimarni  14448  hash2prd  14482  hashle2pr  14484  pr2pwpr  14486  fundmge2nop0  14509  fi1uzind  14514  brfi1indALT  14517  swrdnd2  14663  swrdnnn0nd  14664  swrdnd0  14665  pfxnd0  14696  swrdswrdlem  14711  swrdswrd  14712  ccatopth2  14724  wrd2ind  14730  pfxccatin12lem2a  14734  swrdccatin2  14736  pfxccatin12lem2  14738  pfxccatin12lem3  14739  swrdccat  14742  swrdccat3blem  14746  reuccatpfxs1lem  14753  repswswrd  14791  cshwidxmod  14810  cshwidx0  14813  2cshwcshw  14832  cshwcsh2id  14835  cau3lem  15373  caubnd  15377  climrlim2  15565  rlimcn3  15608  mulcn2  15614  climcau  15689  climbdd  15690  caucvg  15697  modfsummod  15813  p1modz1  16284  dvdsle  16335  dvdsdivcl  16341  ltoddhalfle  16386  halfleoddlt  16387  ndvdssub  16434  gcdcllem1  16524  dvdslegcd  16529  bezoutlem4  16567  dfgcd2  16571  lcmf  16658  lcmfunsnlem1  16662  lcmfunsnlem2lem1  16663  lcmfunsnlem  16666  lcmfdvdsb  16668  lcmfun  16670  coprmdvds1  16677  divgcdcoprm0  16690  cncongr1  16692  cncongr2  16693  prmfac1  16746  pcqcl  16883  dvdsprmpweqle  16913  oddprmdvds  16930  prmpwdvds  16931  infpnlem1  16937  prmgaplem5  17082  prmgaplem6  17083  prmgaplem7  17084  cshwshashlem1  17122  cictr  17829  initoeu2lem1  18038  initoeu2  18040  clatleglb  18541  lidrididd  18695  mulgaddcom  19131  mulginvcom  19132  cycsubm  19234  cyccom  19235  gsmsymgreqlem2  19462  symggen  19501  psgnunilem4  19528  sylow2blem3  19653  frgpnabllem1  19904  imasabl  19907  dprddisj2  20072  lmodfopnelem1  20953  lssssr  21009  lss1d  21018  lspsncv0  21204  rnglidlmcl  21274  rngqiprngimfo  21359  nzerooringczr  21520  pzriprnglem5  21525  pzriprnglem8  21528  znrrg  21605  mplcoe5lem  22080  cply1mul  22347  coe1fzgsumdlem  22354  gsummoncoe1  22359  evl1gsumdlem  22407  mamufacex  22444  dmatelnd  22544  scmataddcl  22564  scmatsubcl  22565  scmatmulcl  22566  smatvscl  22572  mavmulsolcl  22599  mdetdiagid  22648  cramerlem3  22737  pmatcoe1fsupp  22749  cpmatacl  22764  cpmatmcllem  22766  mp2pm2mplem4  22857  chpscmat  22890  chfacfisf  22902  chfacfisfcpmat  22903  uniopn  22945  opnnei  23168  neindisj2  23171  restcls  23229  restntr  23230  tgcnp  23301  subbascn  23302  iscnp4  23311  lpcls  23412  cmpsublem  23447  cmpsub  23448  tgcmp  23449  cmpcld  23450  dfconn2  23467  1stcrest  23501  2ndcdisj  23504  1stccnp  23510  comppfsc  23580  kgencn2  23605  txlm  23696  kqreglem1  23789  filin  23902  isfil2  23904  ufilmax  23955  ufileu  23967  filufint  23968  cfinufil  23976  elfm2  23996  rnelfmlem  24000  rnelfm  24001  flimopn  24023  fbflim2  24025  flffbas  24043  fclsnei  24067  flimfnfcls  24076  fclscmp  24078  fcfnei  24083  cnpfcf  24089  alexsubALTlem2  24096  alexsubALTlem3  24097  alexsubALTlem4  24098  alexsubALT  24099  ptcmplem4  24103  qustgplem  24169  tsmsres  24192  tsmsxp  24203  metss  24556  metcnp3  24588  ovoliunnul  25557  ovolicc2lem3  25569  dyadmax  25648  itg2le  25789  bddiblnc  25892  itgcn  25895  ellimc3  25929  lhop1  26064  dvfsumrlim  26081  fta1g  26218  dvply2g  26337  fta1  26360  aalioulem3  26386  aalioulem4  26387  ulmcaulem  26445  ulmcau  26446  logbgcd1irr  26847  xrlimcnp  27021  cxploglim  27030  jensen  27041  lgsqrmodndvds  27405  gausslemma2dlem1a  27417  gausslemma2dlem2  27419  gausslemma2dlem3  27420  lgsquad2lem2  27437  2lgslem1a1  27441  2sqlem6  27475  2sq2  27485  2sqnn  27491  2sqreultblem  27500  nosepdmlem  27735  nodenselem8  27743  eqcuts3  27885  madebdaylemlrcut  27980  addsprop  28057  addsuniflem  28082  negsprop  28116  mulsprop  28211  mulsuniflem  28230  precsex  28299  onsfi  28437  elnnzs  28482  elreno2  28576  brbtwn2  29063  ax5seglem5  29091  axcontlem4  29125  axcontlem10  29131  umgrnloopv  29264  umgrnloop  29266  upgredgpr  29300  numedglnl  29302  usgrausgrb  29327  usgrnloopvALT  29359  usgrnloopALT  29361  usgredg2vlem2  29384  ushgredgedg  29387  ushgredgedgloop  29389  upgrreslem  29462  umgrreslem  29463  nbgr0edglem  29514  nbusgrvtxm1  29537  uvtxnbgrvtx  29551  cusgredg  29582  cusgrres  29606  cusgrsize2inds  29611  cusgrfi  29616  fusgrregdegfi  29727  ewlkle  29763  uspgr2wlkeqi  29805  lfgrwlkprop  29843  lfgrwlknloop  29845  pthdivtx  29884  2pthnloop  29888  upgrwlkdvdelem  29893  upgrspthswlk  29895  usgr2wlkneq  29913  usgr2trlncl  29917  usgr2pthlem  29920  usgr2pth  29921  uspgrn2crct  29965  crctcshwlkn0lem4  29970  crctcshwlkn0lem5  29971  crctcshwlkn0  29978  wlkiswwlks1  30024  wlkiswwlks2  30032  wlkiswwlksupgr2  30034  wwlksnred  30049  wwlksnext  30050  wwlksnextbi  30051  wwlksnextwrd  30054  wwlksnextinj  30056  wwlksnextproplem2  30067  wwlksnextproplem3  30068  wspthsnonn0vne  30074  wspn0  30081  2pthon3v  30100  usgrwwlks2on  30115  umgrwwlks2on  30116  elwspths2on  30119  elwspths2onw  30120  wpthswwlks2on  30121  clwwlk1loop  30147  clwwlkccatlem  30148  umgrclwwlkge2  30150  clwlkclwwlklem2a4  30156  clwlkclwwlklem2a  30157  clwlkclwwlklem3  30160  clwlkclwwlkf1lem3  30165  clwlkclwwlkfo  30168  clwwisshclwwslemlem  30172  erclwwlkeqlen  30178  erclwwlksym  30180  clwwlkf  30206  clwwlknscsh  30221  erclwwlknsym  30229  clwwlknonex2lem2  30267  clwwlknonex2  30268  upgr3v3e3cycl  30339  upgr4cycl4dv4e  30344  eucrctshift  30402  3vfriswmgr  30437  1to2vfriswmgr  30438  1to3vfriswmgr  30439  n4cyclfrgr  30450  4cyclusnfrgr  30451  frgrnbnb  30452  frgrncvvdeqlem8  30465  frgrwopreg  30482  frgr2wwlk1  30488  frgr2wwlkeqm  30490  2clwwlk2clwwlklem  30505  numclwwlk1lem2fo  30517  wlkl0  30526  numclwlk2lem2f  30536  frgrreggt1  30552  frgrreg  30553  frgrregord013  30554  frgrregord13  30555  frgrogt3nreg  30556  eulplig  30645  nmoub3i  30933  ipasslem5  30995  htthlem  31077  ocin  31456  spansneleq  31730  spansnss  31731  elspansn4  31733  h1datomi  31741  nmopub2tALT  32069  nmfnleub2  32086  hstel2  32379  cvnbtwn  32446  spansncv2  32453  dmdmd  32460  dmdbr3  32465  dmdbr4  32466  dmdbr5  32468  mdsl0  32470  mdexchi  32495  cvexchlem  32528  atcv1  32540  atomli  32542  atcvatlem  32545  atcvat2i  32547  chirredi  32554  mdsymlem3  32565  mdsymlem4  32566  sumdmdii  32575  sumdmdlem  32578  cdj1i  32593  ssrelf  32778  f1o3d  32789  fisshasheq  35426  umgr2cycllem  35451  cvxpconn  35553  satfv0  35669  satfsschain  35675  satfrel  35678  satfdm  35680  satfv0fun  35682  sat1el2xp  35690  gonarlem  35705  goalrlem  35707  satffunlem1lem1  35713  satffunlem2lem1  35715  satffunlem2lem2  35717  satffun  35720  mrsubccat  35829  msubvrs  35871  fundmpss  36078  dfon2lem6  36097  dfon2lem8  36099  dfon2lem9  36100  dfon2  36101  wzel  36133  colinearxfr  36386  btwnconn1lem11  36408  lineintmo  36468  in-ax8  36545  ss-ax8  36546  trer  36637  elicc3  36638  finminlem  36639  nn0prpwlem  36643  fnessref  36678  neibastop2  36682  fgmin  36691  tailfb  36698  ordcmp  36768  ee7.2aOLD  36782  dfttc4  36851  bj-ceqsalt0  37330  bj-ceqsalt1  37331  isbasisrelowllem1  37810  isbasisrelowllem2  37811  relowlpssretop  37819  fvineqsneu  37866  fvineqsneq  37867  wl-mo3t  38040  finixpnum  38065  matunitlindflem1  38076  matunitlindflem2  38077  poimirlem26  38106  poimirlem27  38107  poimirlem29  38109  ftc1anc  38161  fdc  38205  heibor1lem  38269  ghomco  38351  rngoueqz  38400  unichnidl  38491  dmncan1  38536  ax12indn  39528  lshpdisj  39572  lub0N  39774  glb0N  39778  leat2  39879  hlrelat2  39988  cvrexchlem  40004  cvratlem  40006  atcvrj0  40013  cvrat2  40014  snatpsubN  40335  linepsubN  40337  pmaple  40346  pmapsub  40353  elpaddn0  40385  paddasslem5  40409  trlval2  40748  cdlemn11pre  41795  dihord2pre  41810  mapdordlem2  42222  sn-sup2  43074  fsuppind  43133  pell1qrgap  43412  dford3lem1  43564  hbtlem5  43666  onexlimgt  43781  onsucf1olem  43808  omcl2  43871  tfsconcat0b  43884  ntrneiiso  44628  sbiota1  44971  19.41rg  45087  ee223  45171  or2expropbilem1  47587  funressnfv  47598  fcoresf1  47624  2reuimp  47670  f1oresf1o2  47846  zm1nn  47857  nltle2tri  47868  el1fzopredsuc  47881  modlt0b  47924  mod2addne  47925  muldvdsfacgt  47941  muldvdsfacm1  47942  elsetpreimafvssdm  47953  imasetpreimafvbijlemf1  47971  iccpartlt  47991  iccpartgt  47994  iccelpart  48000  icceuelpart  48003  iccpartnel  48005  fargshiftfo  48009  fargshiftfva  48010  lswn0  48011  ich2exprop  48038  prsprel  48054  sprsymrelfolem2  48060  sprsymrelfo  48064  poprelb  48091  reuopreuprim  48093  goldbachthlem2  48116  odz2prm2pw  48133  fmtnoprmfac1  48135  fmtnofac2lem  48138  prmdvdsfmtnof1lem2  48155  2pwp1prm  48159  sfprmdvdsmersenne  48173  lighneallem3  48177  requad01  48204  requad2  48206  even3prm2  48302  fppr2odd  48314  fpprwpprb  48323  gbegt5  48344  sbgoldbwt  48360  sbgoldbalt  48364  sbgoldbm  48367  bgoldbtbndlem2  48389  bgoldbtbndlem3  48390  bgoldbtbndlem4  48391  bgoldbtbnd  48392  tgblthelfgott  48398  tgoldbach  48400  isubgredg  48449  grimuhgr  48470  grimcnv  48471  grimco  48472  isuspgrim0  48477  isuspgrimlem  48478  uhgrimisgrgriclem  48513  clnbgrgrimlem  48516  grimedg  48518  grtriprop  48524  cycl3grtri  48530  grimgrtri  48532  isubgr3stgrlem6  48554  uspgrlimlem3  48573  uspgrlimlem4  48574  grlimgrtrilem2  48585  grlicsym  48596  clnbgr3stgrgrlim  48602  clnbgr3stgrgrlic  48603  gpgedg2ov  48649  gpgedg2iv  48650  pgnbgreunbgrlem3  48701  pgnbgreunbgrlem6  48707  upgrwlkupwlk  48723  lmod0rng  48812  ztprmneprm  48930  ply1mulgsumlem1  48969  ply1mulgsumlem2  48970  lcoel0  49011  linindslinci  49031  lindslinindimp2lem4  49044  lindslinindsimp2lem5  49045  snlindsntor  49054  ldepspr  49056  lincresunit2  49061  fllog2  49151  dignn0ldlem  49185  dignn0flhalflem1  49198  nn0sumshdiglemA  49202  nn0sumshdiglemB  49203  itcovalt2  49260  resum2sqorgt0  49292  eenglngeehlnmlem2  49321  rrx2linest  49325  itscnhlc0xyqsol  49348  itsclc0  49354  setrec1lem2  50270  aacllem  50383