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  846  dedlem0b  1045  sbequ1  2256  moexexlem  2627  ralrimdvva  3193  ceqsal1t  3475  ceqsalt  3476  spcimgft  3505  vtoclgft  3511  elabgtOLD  3629  sbciegftOLD  3780  reupick  4283  reusv3  5352  sbcop1  5444  propeqop  5463  pwssun  5524  wefrc  5626  ssrel  5740  ssrel2  5742  ssrelrel  5753  ssrelrn  5851  tz7.7  6351  ordtr2  6370  onmindif  6419  unizlim  6449  funssres  6544  f1ssf1  6814  fvmptt  6970  fveqdmss  7032  fvcofneq  7047  funsndifnop  7106  funfvima2  7187  isoini  7294  isopolem  7301  weniso  7310  f1ocnv2d  7621  limsssuc  7802  tfindsg  7813  limomss  7823  findsg  7849  funcnvuni  7884  f1oweALT  7926  funelss  8001  bropopvvv  8042  bropfvvvvlem  8043  bropfvvvv  8044  f1o2ndf1  8074  frxp  8078  soseq  8111  suppfnss  8141  onfununi  8283  tz7.49  8386  omordi  8503  omlimcl  8515  omass  8517  oeordsuc  8532  nnmordi  8569  nnmord  8570  omabs  8589  xpdom2  9012  infensuc  9095  findcard2  9101  findcard2d  9103  findcard3  9195  frfi  9197  fsuppres  9308  dffi2  9338  elfiun  9345  ordiso2  9432  ordtypelem7  9441  suc11reg  9540  inf3lem2  9550  noinfep  9581  cantnfle  9592  cantnflem1  9610  cantnf  9614  ttrclss  9641  trcl  9649  epfrs  9652  frr3g  9680  r1sdom  9698  updjud  9858  dfac8alem  9951  indcardi  9963  alephordi  9996  dfac12lem3  10068  pwsdompw  10125  cofsmo  10191  cfcoflem  10194  coftr  10195  isf32lem2  10276  isf32lem9  10283  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  zorn2lem4  10421  zorn2lem6  10423  zorn2lem7  10424  ttukeylem6  10436  uniimadom  10466  konigthlem  10491  fpwwe2lem7  10560  tskord  10703  tskcard  10704  grupr  10720  gruiin  10733  grudomon  10740  grur1a  10742  genpn0  10926  genpcd  10929  distrlem5pr  10950  psslinpr  10954  ltaddpr  10957  ltexprlem3  10961  ltexprlem6  10964  ltapr  10968  prlem936  10970  suplem1pr  10975  axpre-sup  11092  1re  11144  dedekindle  11309  lemul12a  12011  divgt0  12022  divge0  12023  lbreu  12104  sup2  12110  bndndx  12412  elnnz  12510  nzadd  12551  fzind  12602  fnn0ind  12603  uzwo  12836  lbzbi  12861  zmax  12870  zbtwnre  12871  irradd  12898  irrmul  12899  ledivge1le  12990  xrub  13239  supxrunb2  13247  infmremnf  13271  iccid  13318  uzsubsubfz  13474  fzrevral  13540  elfz0fzfz0  13561  fz0fzelfz0  13562  elfzmlbp  13567  elincfzoext  13651  ssfzoulel  13688  ssfzo12bi  13689  fzoopth  13690  elfzonelfzo  13697  elfznelfzo  13701  elfznelfzob  13702  injresinjlem  13718  fleqceilz  13786  modaddmodup  13869  uzindi  13917  suppssfz  13929  mptnn0fsuppr  13934  le2sq2  14070  sqlecan  14144  facdiv  14222  facwordi  14224  faclbnd  14225  hashimarni  14376  hash2prd  14410  hashle2pr  14412  pr2pwpr  14414  fundmge2nop0  14437  fi1uzind  14442  brfi1indALT  14445  swrdnd2  14591  swrdnnn0nd  14592  swrdnd0  14593  pfxnd0  14624  swrdswrdlem  14639  swrdswrd  14640  ccatopth2  14652  wrd2ind  14658  pfxccatin12lem2a  14662  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12lem3  14667  swrdccat  14670  swrdccat3blem  14674  reuccatpfxs1lem  14681  repswswrd  14719  cshwidxmod  14738  cshwidx0  14741  2cshwcshw  14760  cshwcsh2id  14763  cau3lem  15290  caubnd  15294  climrlim2  15482  rlimcn3  15525  mulcn2  15531  climcau  15606  climbdd  15607  caucvg  15614  modfsummod  15729  p1modz1  16198  dvdsle  16249  dvdsdivcl  16255  ltoddhalfle  16300  halfleoddlt  16301  ndvdssub  16348  gcdcllem1  16438  dvdslegcd  16443  bezoutlem4  16481  dfgcd2  16485  lcmf  16572  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem  16580  lcmfdvdsb  16582  lcmfun  16584  coprmdvds1  16591  divgcdcoprm0  16604  cncongr1  16606  cncongr2  16607  prmfac1  16659  pcqcl  16796  dvdsprmpweqle  16826  oddprmdvds  16843  prmpwdvds  16844  infpnlem1  16850  prmgaplem5  16995  prmgaplem6  16996  prmgaplem7  16997  cshwshashlem1  17035  cictr  17741  initoeu2lem1  17950  initoeu2  17952  clatleglb  18453  lidrididd  18607  mulgaddcom  19040  mulginvcom  19041  cycsubm  19143  cyccom  19144  gsmsymgreqlem2  19372  symggen  19411  psgnunilem4  19438  sylow2blem3  19563  frgpnabllem1  19814  imasabl  19817  dprddisj2  19982  lmodfopnelem1  20861  lssssr  20917  lss1d  20926  lspsncv0  21113  rnglidlmcl  21183  rngqiprngimfo  21268  nzerooringczr  21447  pzriprnglem5  21452  pzriprnglem8  21455  znrrg  21532  mplcoe5lem  22006  cply1mul  22252  coe1fzgsumdlem  22259  gsummoncoe1  22264  evl1gsumdlem  22312  mamufacex  22352  dmatelnd  22452  scmataddcl  22472  scmatsubcl  22473  scmatmulcl  22474  smatvscl  22480  mavmulsolcl  22507  mdetdiagid  22556  cramerlem3  22645  pmatcoe1fsupp  22657  cpmatacl  22672  cpmatmcllem  22674  mp2pm2mplem4  22765  chpscmat  22798  chfacfisf  22810  chfacfisfcpmat  22811  uniopn  22853  opnnei  23076  neindisj2  23079  restcls  23137  restntr  23138  tgcnp  23209  subbascn  23210  iscnp4  23219  lpcls  23320  cmpsublem  23355  cmpsub  23356  tgcmp  23357  cmpcld  23358  dfconn2  23375  1stcrest  23409  2ndcdisj  23412  1stccnp  23418  comppfsc  23488  kgencn2  23513  txlm  23604  kqreglem1  23697  filin  23810  isfil2  23812  ufilmax  23863  ufileu  23875  filufint  23876  cfinufil  23884  elfm2  23904  rnelfmlem  23908  rnelfm  23909  flimopn  23931  fbflim2  23933  flffbas  23951  fclsnei  23975  flimfnfcls  23984  fclscmp  23986  fcfnei  23991  cnpfcf  23997  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  ptcmplem4  24011  qustgplem  24077  tsmsres  24100  tsmsxp  24111  metss  24464  metcnp3  24496  ovoliunnul  25476  ovolicc2lem3  25488  dyadmax  25567  itg2le  25708  bddiblnc  25811  itgcn  25814  ellimc3  25848  lhop1  25987  dvfsumrlim  26006  fta1g  26143  dvply2g  26260  fta1  26284  aalioulem3  26310  aalioulem4  26311  ulmcaulem  26371  ulmcau  26372  logbgcd1irr  26772  xrlimcnp  26946  cxploglim  26956  jensen  26967  lgsqrmodndvds  27332  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem3  27347  lgsquad2lem2  27364  2lgslem1a1  27368  2sqlem6  27402  2sq2  27412  2sqnn  27418  2sqreultblem  27427  nosepdmlem  27663  nodenselem8  27671  eqcuts3  27812  madebdaylemlrcut  27907  addsprop  27984  addsuniflem  28009  negsprop  28043  mulsprop  28138  mulsuniflem  28157  precsex  28226  onsfi  28364  elnnzs  28409  elreno2  28503  brbtwn2  28990  ax5seglem5  29018  axcontlem4  29052  axcontlem10  29058  umgrnloopv  29191  umgrnloop  29193  upgredgpr  29227  numedglnl  29229  usgrausgrb  29254  usgrnloopvALT  29286  usgrnloopALT  29288  usgredg2vlem2  29311  ushgredgedg  29314  ushgredgedgloop  29316  upgrreslem  29389  umgrreslem  29390  nbgr0edglem  29441  nbusgrvtxm1  29464  uvtxnbgrvtx  29478  cusgredg  29509  cusgrres  29534  cusgrsize2inds  29539  cusgrfi  29544  fusgrregdegfi  29655  ewlkle  29691  uspgr2wlkeqi  29733  lfgrwlkprop  29771  lfgrwlknloop  29773  pthdivtx  29812  2pthnloop  29816  upgrwlkdvdelem  29821  upgrspthswlk  29823  usgr2wlkneq  29841  usgr2trlncl  29845  usgr2pthlem  29848  usgr2pth  29849  uspgrn2crct  29893  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0  29906  wlkiswwlks1  29952  wlkiswwlks2  29960  wlkiswwlksupgr2  29962  wwlksnred  29977  wwlksnext  29978  wwlksnextbi  29979  wwlksnextwrd  29982  wwlksnextinj  29984  wwlksnextproplem2  29995  wwlksnextproplem3  29996  wspthsnonn0vne  30002  wspn0  30009  2pthon3v  30028  usgrwwlks2on  30043  umgrwwlks2on  30044  elwspths2on  30047  elwspths2onw  30048  wpthswwlks2on  30049  clwwlk1loop  30075  clwwlkccatlem  30076  umgrclwwlkge2  30078  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem3  30088  clwlkclwwlkf1lem3  30093  clwlkclwwlkfo  30096  clwwisshclwwslemlem  30100  erclwwlkeqlen  30106  erclwwlksym  30108  clwwlkf  30134  clwwlknscsh  30149  erclwwlknsym  30157  clwwlknonex2lem2  30195  clwwlknonex2  30196  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eucrctshift  30330  3vfriswmgr  30365  1to2vfriswmgr  30366  1to3vfriswmgr  30367  n4cyclfrgr  30378  4cyclusnfrgr  30379  frgrnbnb  30380  frgrncvvdeqlem8  30393  frgrwopreg  30410  frgr2wwlk1  30416  frgr2wwlkeqm  30418  2clwwlk2clwwlklem  30433  numclwwlk1lem2fo  30445  wlkl0  30454  numclwlk2lem2f  30464  frgrreggt1  30480  frgrreg  30481  frgrregord013  30482  frgrregord13  30483  frgrogt3nreg  30484  eulplig  30573  nmoub3i  30861  ipasslem5  30923  htthlem  31005  ocin  31384  spansneleq  31658  spansnss  31659  elspansn4  31661  h1datomi  31669  nmopub2tALT  31997  nmfnleub2  32014  hstel2  32307  cvnbtwn  32374  spansncv2  32381  dmdmd  32388  dmdbr3  32393  dmdbr4  32394  dmdbr5  32396  mdsl0  32398  mdexchi  32423  cvexchlem  32456  atcv1  32468  atomli  32470  atcvatlem  32473  atcvat2i  32475  chirredi  32482  mdsymlem3  32493  mdsymlem4  32494  sumdmdii  32503  sumdmdlem  32506  cdj1i  32521  ssrelf  32705  f1o3d  32716  fisshasheq  35331  umgr2cycllem  35356  cvxpconn  35458  satfv0  35574  satfsschain  35580  satfrel  35583  satfdm  35585  satfv0fun  35587  sat1el2xp  35595  gonarlem  35610  goalrlem  35612  satffunlem1lem1  35618  satffunlem2lem1  35620  satffunlem2lem2  35622  satffun  35625  mrsubccat  35734  msubvrs  35776  fundmpss  35983  dfon2lem6  36002  dfon2lem8  36004  dfon2lem9  36005  dfon2  36006  wzel  36038  colinearxfr  36291  btwnconn1lem11  36313  lineintmo  36373  in-ax8  36440  ss-ax8  36441  trer  36532  elicc3  36533  finminlem  36534  nn0prpwlem  36538  fnessref  36573  neibastop2  36577  fgmin  36586  tailfb  36593  ordcmp  36663  ee7.2aOLD  36677  bj-cbvalimt  36875  bj-ceqsalt0  37132  bj-ceqsalt1  37133  isbasisrelowllem1  37610  isbasisrelowllem2  37611  relowlpssretop  37619  fvineqsneu  37666  fvineqsneq  37667  wl-mo3t  37831  finixpnum  37856  matunitlindflem1  37867  matunitlindflem2  37868  poimirlem26  37897  poimirlem27  37898  poimirlem29  37900  ftc1anc  37952  fdc  37996  heibor1lem  38060  ghomco  38142  rngoueqz  38191  unichnidl  38282  dmncan1  38327  ax12indn  39319  lshpdisj  39363  lub0N  39565  glb0N  39569  leat2  39670  hlrelat2  39779  cvrexchlem  39795  cvratlem  39797  atcvrj0  39804  cvrat2  39805  snatpsubN  40126  linepsubN  40128  pmaple  40137  pmapsub  40144  elpaddn0  40176  paddasslem5  40200  trlval2  40539  cdlemn11pre  41586  dihord2pre  41601  mapdordlem2  42013  sn-sup2  42861  fsuppind  42948  pell1qrgap  43231  dford3lem1  43383  hbtlem5  43485  onexlimgt  43600  onsucf1olem  43627  omcl2  43690  tfsconcat0b  43703  ntrneiiso  44447  sbiota1  44790  19.41rg  44906  ee223  44990  or2expropbilem1  47392  funressnfv  47403  fcoresf1  47429  2reuimp  47475  f1oresf1o2  47651  zm1nn  47662  nltle2tri  47673  el1fzopredsuc  47685  modlt0b  47723  mod2addne  47724  elsetpreimafvssdm  47746  imasetpreimafvbijlemf1  47764  iccpartlt  47784  iccpartgt  47787  iccelpart  47793  icceuelpart  47796  iccpartnel  47798  fargshiftfo  47802  fargshiftfva  47803  lswn0  47804  ich2exprop  47831  prsprel  47847  sprsymrelfolem2  47853  sprsymrelfo  47857  poprelb  47884  reuopreuprim  47886  goldbachthlem2  47906  odz2prm2pw  47923  fmtnoprmfac1  47925  fmtnofac2lem  47928  prmdvdsfmtnof1lem2  47945  2pwp1prm  47949  sfprmdvdsmersenne  47963  lighneallem3  47967  requad01  47981  requad2  47983  even3prm2  48079  fppr2odd  48091  fpprwpprb  48100  gbegt5  48121  sbgoldbwt  48137  sbgoldbalt  48141  sbgoldbm  48144  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  bgoldbtbnd  48169  tgblthelfgott  48175  tgoldbach  48177  isubgredg  48226  grimuhgr  48247  grimcnv  48248  grimco  48249  isuspgrim0  48254  isuspgrimlem  48255  uhgrimisgrgriclem  48290  clnbgrgrimlem  48293  grimedg  48295  grtriprop  48301  cycl3grtri  48307  grimgrtri  48309  isubgr3stgrlem6  48331  uspgrlimlem3  48350  uspgrlimlem4  48351  grlimgrtrilem2  48362  grlicsym  48373  clnbgr3stgrgrlim  48379  clnbgr3stgrgrlic  48380  gpgedg2ov  48426  gpgedg2iv  48427  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  upgrwlkupwlk  48500  lmod0rng  48589  ztprmneprm  48707  ply1mulgsumlem1  48746  ply1mulgsumlem2  48747  lcoel0  48788  linindslinci  48808  lindslinindimp2lem4  48821  lindslinindsimp2lem5  48822  snlindsntor  48831  ldepspr  48833  lincresunit2  48838  fllog2  48928  dignn0ldlem  48962  dignn0flhalflem1  48975  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  itcovalt2  49037  resum2sqorgt0  49069  eenglngeehlnmlem2  49098  rrx2linest  49102  itscnhlc0xyqsol  49125  itsclc0  49131  setrec1lem2  50047  aacllem  50160