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  2253  moexexlem  2623  ralrimdvva  3188  ceqsal1t  3470  ceqsalt  3471  spcimgft  3500  vtoclgft  3506  elabgtOLD  3624  sbciegftOLD  3775  reupick  4278  reusv3  5345  sbcop1  5431  propeqop  5450  pwssun  5511  wefrc  5613  ssrel  5727  ssrel2  5729  ssrelrel  5740  ssrelrn  5838  tz7.7  6337  ordtr2  6356  onmindif  6405  unizlim  6435  funssres  6530  f1ssf1  6800  fvmptt  6955  fveqdmss  7017  fvcofneq  7032  funsndifnop  7090  funfvima2  7171  isoini  7278  isopolem  7285  weniso  7294  f1ocnv2d  7605  limsssuc  7786  tfindsg  7797  limomss  7807  findsg  7833  funcnvuni  7868  f1oweALT  7910  funelss  7985  bropopvvv  8026  bropfvvvvlem  8027  bropfvvvv  8028  f1o2ndf1  8058  frxp  8062  soseq  8095  suppfnss  8125  onfununi  8267  tz7.49  8370  omordi  8487  omlimcl  8499  omass  8501  oeordsuc  8515  nnmordi  8552  nnmord  8553  omabs  8572  xpdom2  8992  infensuc  9075  findcard2  9081  findcard2d  9083  findcard3  9174  frfi  9176  fsuppres  9284  dffi2  9314  elfiun  9321  ordiso2  9408  ordtypelem7  9417  suc11reg  9516  inf3lem2  9526  noinfep  9557  cantnfle  9568  cantnflem1  9586  cantnf  9590  ttrclss  9617  trcl  9625  epfrs  9628  frr3g  9656  r1sdom  9674  updjud  9834  dfac8alem  9927  indcardi  9939  alephordi  9972  dfac12lem3  10044  pwsdompw  10101  cofsmo  10167  cfcoflem  10170  coftr  10171  isf32lem2  10252  isf32lem9  10259  axcc3  10336  domtriomlem  10340  axdc3lem2  10349  axdc3lem4  10351  zorn2lem4  10397  zorn2lem6  10399  zorn2lem7  10400  ttukeylem6  10412  uniimadom  10442  konigthlem  10466  fpwwe2lem7  10535  tskord  10678  tskcard  10679  grupr  10695  gruiin  10708  grudomon  10715  grur1a  10717  genpn0  10901  genpcd  10904  distrlem5pr  10925  psslinpr  10929  ltaddpr  10932  ltexprlem3  10936  ltexprlem6  10939  ltapr  10943  prlem936  10945  suplem1pr  10950  axpre-sup  11067  1re  11119  dedekindle  11284  lemul12a  11986  divgt0  11997  divge0  11998  lbreu  12079  sup2  12085  bndndx  12387  elnnz  12485  nzadd  12526  fzind  12577  fnn0ind  12578  uzwo  12811  lbzbi  12836  zmax  12845  zbtwnre  12846  irradd  12873  irrmul  12874  ledivge1le  12965  xrub  13213  supxrunb2  13221  infmremnf  13245  iccid  13292  uzsubsubfz  13448  fzrevral  13514  elfz0fzfz0  13535  fz0fzelfz0  13536  elfzmlbp  13541  elincfzoext  13625  ssfzoulel  13662  ssfzo12bi  13663  fzoopth  13664  elfzonelfzo  13671  elfznelfzo  13675  elfznelfzob  13676  injresinjlem  13692  fleqceilz  13760  modaddmodup  13843  uzindi  13891  suppssfz  13903  mptnn0fsuppr  13908  le2sq2  14044  sqlecan  14118  facdiv  14196  facwordi  14198  faclbnd  14199  hashimarni  14350  hash2prd  14384  hashle2pr  14386  pr2pwpr  14388  fundmge2nop0  14411  fi1uzind  14416  brfi1indALT  14419  swrdnd2  14565  swrdnnn0nd  14566  swrdnd0  14567  pfxnd0  14598  swrdswrdlem  14613  swrdswrd  14614  ccatopth2  14626  wrd2ind  14632  pfxccatin12lem2a  14636  swrdccatin2  14638  pfxccatin12lem2  14640  pfxccatin12lem3  14641  swrdccat  14644  swrdccat3blem  14648  reuccatpfxs1lem  14655  repswswrd  14693  cshwidxmod  14712  cshwidx0  14715  2cshwcshw  14734  cshwcsh2id  14737  cau3lem  15264  caubnd  15268  climrlim2  15456  rlimcn3  15499  mulcn2  15505  climcau  15580  climbdd  15581  caucvg  15588  modfsummod  15703  p1modz1  16172  dvdsle  16223  dvdsdivcl  16229  ltoddhalfle  16274  halfleoddlt  16275  ndvdssub  16322  gcdcllem1  16412  dvdslegcd  16417  bezoutlem4  16455  dfgcd2  16459  lcmf  16546  lcmfunsnlem1  16550  lcmfunsnlem2lem1  16551  lcmfunsnlem  16554  lcmfdvdsb  16556  lcmfun  16558  coprmdvds1  16565  divgcdcoprm0  16578  cncongr1  16580  cncongr2  16581  prmfac1  16633  pcqcl  16770  dvdsprmpweqle  16800  oddprmdvds  16817  prmpwdvds  16818  infpnlem1  16824  prmgaplem5  16969  prmgaplem6  16970  prmgaplem7  16971  cshwshashlem1  17009  cictr  17714  initoeu2lem1  17923  initoeu2  17925  clatleglb  18426  lidrididd  18580  mulgaddcom  19013  mulginvcom  19014  cycsubm  19116  cyccom  19117  gsmsymgreqlem2  19345  symggen  19384  psgnunilem4  19411  sylow2blem3  19536  frgpnabllem1  19787  imasabl  19790  dprddisj2  19955  lmodfopnelem1  20833  lssssr  20889  lss1d  20898  lspsncv0  21085  rnglidlmcl  21155  rngqiprngimfo  21240  nzerooringczr  21419  pzriprnglem5  21424  pzriprnglem8  21427  znrrg  21504  mplcoe5lem  21975  cply1mul  22212  coe1fzgsumdlem  22219  gsummoncoe1  22224  evl1gsumdlem  22272  mamufacex  22312  dmatelnd  22412  scmataddcl  22432  scmatsubcl  22433  scmatmulcl  22434  smatvscl  22440  mavmulsolcl  22467  mdetdiagid  22516  cramerlem3  22605  pmatcoe1fsupp  22617  cpmatacl  22632  cpmatmcllem  22634  mp2pm2mplem4  22725  chpscmat  22758  chfacfisf  22770  chfacfisfcpmat  22771  uniopn  22813  opnnei  23036  neindisj2  23039  restcls  23097  restntr  23098  tgcnp  23169  subbascn  23170  iscnp4  23179  lpcls  23280  cmpsublem  23315  cmpsub  23316  tgcmp  23317  cmpcld  23318  dfconn2  23335  1stcrest  23369  2ndcdisj  23372  1stccnp  23378  comppfsc  23448  kgencn2  23473  txlm  23564  kqreglem1  23657  filin  23770  isfil2  23772  ufilmax  23823  ufileu  23835  filufint  23836  cfinufil  23844  elfm2  23864  rnelfmlem  23868  rnelfm  23869  flimopn  23891  fbflim2  23893  flffbas  23911  fclsnei  23935  flimfnfcls  23944  fclscmp  23946  fcfnei  23951  cnpfcf  23957  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALTlem4  23966  alexsubALT  23967  ptcmplem4  23971  qustgplem  24037  tsmsres  24060  tsmsxp  24071  metss  24424  metcnp3  24456  ovoliunnul  25436  ovolicc2lem3  25448  dyadmax  25527  itg2le  25668  bddiblnc  25771  itgcn  25774  ellimc3  25808  lhop1  25947  dvfsumrlim  25966  fta1g  26103  dvply2g  26220  fta1  26244  aalioulem3  26270  aalioulem4  26271  ulmcaulem  26331  ulmcau  26332  logbgcd1irr  26732  xrlimcnp  26906  cxploglim  26916  jensen  26927  lgsqrmodndvds  27292  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  gausslemma2dlem3  27307  lgsquad2lem2  27324  2lgslem1a1  27328  2sqlem6  27362  2sq2  27372  2sqnn  27378  2sqreultblem  27387  nosepdmlem  27623  nodenselem8  27631  eqscut3  27766  madebdaylemlrcut  27845  addsprop  27920  addsuniflem  27945  negsprop  27978  mulsprop  28070  mulsuniflem  28089  precsex  28157  onsfi  28284  elnnzs  28326  brbtwn2  28885  ax5seglem5  28913  axcontlem4  28947  axcontlem10  28953  umgrnloopv  29086  umgrnloop  29088  upgredgpr  29122  numedglnl  29124  usgrausgrb  29149  usgrnloopvALT  29181  usgrnloopALT  29183  usgredg2vlem2  29206  ushgredgedg  29209  ushgredgedgloop  29211  upgrreslem  29284  umgrreslem  29285  nbgr0edglem  29336  nbusgrvtxm1  29359  uvtxnbgrvtx  29373  cusgredg  29404  cusgrres  29429  cusgrsize2inds  29434  cusgrfi  29439  fusgrregdegfi  29550  ewlkle  29586  uspgr2wlkeqi  29628  lfgrwlkprop  29666  lfgrwlknloop  29668  pthdivtx  29707  2pthnloop  29711  upgrwlkdvdelem  29716  upgrspthswlk  29718  usgr2wlkneq  29736  usgr2trlncl  29740  usgr2pthlem  29743  usgr2pth  29744  uspgrn2crct  29788  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshwlkn0  29801  wlkiswwlks1  29847  wlkiswwlks2  29855  wlkiswwlksupgr2  29857  wwlksnred  29872  wwlksnext  29873  wwlksnextbi  29874  wwlksnextwrd  29877  wwlksnextinj  29879  wwlksnextproplem2  29890  wwlksnextproplem3  29891  wspthsnonn0vne  29897  wspn0  29904  2pthon3v  29923  usgrwwlks2on  29938  umgrwwlks2on  29939  elwspths2on  29942  elwspths2onw  29943  wpthswwlks2on  29944  clwwlk1loop  29970  clwwlkccatlem  29971  umgrclwwlkge2  29973  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwlkclwwlklem3  29983  clwlkclwwlkf1lem3  29988  clwlkclwwlkfo  29991  clwwisshclwwslemlem  29995  erclwwlkeqlen  30001  erclwwlksym  30003  clwwlkf  30029  clwwlknscsh  30044  erclwwlknsym  30052  clwwlknonex2lem2  30090  clwwlknonex2  30091  upgr3v3e3cycl  30162  upgr4cycl4dv4e  30167  eucrctshift  30225  3vfriswmgr  30260  1to2vfriswmgr  30261  1to3vfriswmgr  30262  n4cyclfrgr  30273  4cyclusnfrgr  30274  frgrnbnb  30275  frgrncvvdeqlem8  30288  frgrwopreg  30305  frgr2wwlk1  30311  frgr2wwlkeqm  30313  2clwwlk2clwwlklem  30328  numclwwlk1lem2fo  30340  wlkl0  30349  numclwlk2lem2f  30359  frgrreggt1  30375  frgrreg  30376  frgrregord013  30377  frgrregord13  30378  frgrogt3nreg  30379  eulplig  30467  nmoub3i  30755  ipasslem5  30817  htthlem  30899  ocin  31278  spansneleq  31552  spansnss  31553  elspansn4  31555  h1datomi  31563  nmopub2tALT  31891  nmfnleub2  31908  hstel2  32201  cvnbtwn  32268  spansncv2  32275  dmdmd  32282  dmdbr3  32287  dmdbr4  32288  dmdbr5  32290  mdsl0  32292  mdexchi  32317  cvexchlem  32350  atcv1  32362  atomli  32364  atcvatlem  32367  atcvat2i  32369  chirredi  32376  mdsymlem3  32387  mdsymlem4  32388  sumdmdii  32397  sumdmdlem  32400  cdj1i  32415  ssrelf  32600  f1o3d  32610  fisshasheq  35180  umgr2cycllem  35205  cvxpconn  35307  satfv0  35423  satfsschain  35429  satfrel  35432  satfdm  35434  satfv0fun  35436  sat1el2xp  35444  gonarlem  35459  goalrlem  35461  satffunlem1lem1  35467  satffunlem2lem1  35469  satffunlem2lem2  35471  satffun  35474  mrsubccat  35583  msubvrs  35625  fundmpss  35832  dfon2lem6  35851  dfon2lem8  35853  dfon2lem9  35854  dfon2  35855  wzel  35887  colinearxfr  36140  btwnconn1lem11  36162  lineintmo  36222  in-ax8  36289  ss-ax8  36290  trer  36381  elicc3  36382  finminlem  36383  nn0prpwlem  36387  fnessref  36422  neibastop2  36426  fgmin  36435  tailfb  36442  ordcmp  36512  ee7.2aOLD  36526  bj-cbvalimt  36704  bj-ceqsalt0  36949  bj-ceqsalt1  36950  isbasisrelowllem1  37420  isbasisrelowllem2  37421  relowlpssretop  37429  fvineqsneu  37476  fvineqsneq  37477  wl-mo3t  37641  finixpnum  37666  matunitlindflem1  37677  matunitlindflem2  37678  poimirlem26  37707  poimirlem27  37708  poimirlem29  37710  ftc1anc  37762  fdc  37806  heibor1lem  37870  ghomco  37952  rngoueqz  38001  unichnidl  38092  dmncan1  38137  ax12indn  39063  lshpdisj  39107  lub0N  39309  glb0N  39313  leat2  39414  hlrelat2  39523  cvrexchlem  39539  cvratlem  39541  atcvrj0  39548  cvrat2  39549  snatpsubN  39870  linepsubN  39872  pmaple  39881  pmapsub  39888  elpaddn0  39920  paddasslem5  39944  trlval2  40283  cdlemn11pre  41330  dihord2pre  41345  mapdordlem2  41757  sn-sup2  42610  fsuppind  42709  pell1qrgap  42992  dford3lem1  43144  hbtlem5  43246  onexlimgt  43361  onsucf1olem  43388  omcl2  43451  tfsconcat0b  43464  ntrneiiso  44209  sbiota1  44552  19.41rg  44668  ee223  44752  or2expropbilem1  47157  funressnfv  47168  fcoresf1  47194  2reuimp  47240  f1oresf1o2  47416  zm1nn  47427  nltle2tri  47438  el1fzopredsuc  47450  modlt0b  47488  mod2addne  47489  elsetpreimafvssdm  47511  imasetpreimafvbijlemf1  47529  iccpartlt  47549  iccpartgt  47552  iccelpart  47558  icceuelpart  47561  iccpartnel  47563  fargshiftfo  47567  fargshiftfva  47568  lswn0  47569  ich2exprop  47596  prsprel  47612  sprsymrelfolem2  47618  sprsymrelfo  47622  poprelb  47649  reuopreuprim  47651  goldbachthlem2  47671  odz2prm2pw  47688  fmtnoprmfac1  47690  fmtnofac2lem  47693  prmdvdsfmtnof1lem2  47710  2pwp1prm  47714  sfprmdvdsmersenne  47728  lighneallem3  47732  requad01  47746  requad2  47748  even3prm2  47844  fppr2odd  47856  fpprwpprb  47865  gbegt5  47886  sbgoldbwt  47902  sbgoldbalt  47906  sbgoldbm  47909  bgoldbtbndlem2  47931  bgoldbtbndlem3  47932  bgoldbtbndlem4  47933  bgoldbtbnd  47934  tgblthelfgott  47940  tgoldbach  47942  isubgredg  47991  grimuhgr  48012  grimcnv  48013  grimco  48014  isuspgrim0  48019  isuspgrimlem  48020  uhgrimisgrgriclem  48055  clnbgrgrimlem  48058  grimedg  48060  grtriprop  48066  cycl3grtri  48072  grimgrtri  48074  isubgr3stgrlem6  48096  uspgrlimlem3  48115  uspgrlimlem4  48116  grlimgrtrilem2  48127  grlicsym  48138  clnbgr3stgrgrlim  48144  clnbgr3stgrgrlic  48145  gpgedg2ov  48191  gpgedg2iv  48192  pgnbgreunbgrlem3  48243  pgnbgreunbgrlem6  48249  upgrwlkupwlk  48265  lmod0rng  48354  ztprmneprm  48472  ply1mulgsumlem1  48512  ply1mulgsumlem2  48513  lcoel0  48554  linindslinci  48574  lindslinindimp2lem4  48587  lindslinindsimp2lem5  48588  snlindsntor  48597  ldepspr  48599  lincresunit2  48604  fllog2  48694  dignn0ldlem  48728  dignn0flhalflem1  48741  nn0sumshdiglemA  48745  nn0sumshdiglemB  48746  itcovalt2  48803  resum2sqorgt0  48835  eenglngeehlnmlem2  48864  rrx2linest  48868  itscnhlc0xyqsol  48891  itsclc0  48897  setrec1lem2  49814  aacllem  49927