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  3192  ceqsal1t  3480  ceqsalt  3481  spcimgft  3512  vtoclgft  3518  elabgtOLD  3639  sbciegftOLD  3791  reupick  4292  reusv3  5360  sbcop1  5448  propeqop  5467  pwssun  5530  wefrc  5632  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  ssrelrn  5858  tz7.7  6358  ordtr2  6377  onmindif  6426  unizlim  6457  funssres  6560  f1ssf1  6832  fvmptt  6988  fveqdmss  7050  fvcofneq  7065  funsndifnop  7123  funfvima2  7205  isoini  7313  isopolem  7320  weniso  7329  f1ocnv2d  7642  limsssuc  7826  tfindsg  7837  limomss  7847  findsg  7873  funcnvuni  7908  f1oweALT  7951  funelss  8026  bropopvvv  8069  bropfvvvvlem  8070  bropfvvvv  8071  f1o2ndf1  8101  frxp  8105  soseq  8138  suppfnss  8168  onfununi  8310  tz7.49  8413  omordi  8530  omlimcl  8542  omass  8544  oeordsuc  8558  nnmordi  8595  nnmord  8596  omabs  8615  xpdom2  9036  infensuc  9119  findcard2  9128  findcard2d  9130  findcard3  9229  findcard3OLD  9230  frfi  9232  xpfiOLD  9270  fsuppres  9344  dffi2  9374  elfiun  9381  ordiso2  9468  ordtypelem7  9477  suc11reg  9572  inf3lem2  9582  noinfep  9613  cantnfle  9624  cantnflem1  9642  cantnf  9646  ttrclss  9673  trcl  9681  epfrs  9684  frr3g  9709  r1sdom  9727  updjud  9887  pr2neOLD  9958  dfac8alem  9982  indcardi  9994  alephordi  10027  dfac12lem3  10099  pwsdompw  10156  cofsmo  10222  cfcoflem  10225  coftr  10226  isf32lem2  10307  isf32lem9  10314  axcc3  10391  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  zorn2lem4  10452  zorn2lem6  10454  zorn2lem7  10455  ttukeylem6  10467  uniimadom  10497  konigthlem  10521  fpwwe2lem7  10590  tskord  10733  tskcard  10734  grupr  10750  gruiin  10763  grudomon  10770  grur1a  10772  genpn0  10956  genpcd  10959  distrlem5pr  10980  psslinpr  10984  ltaddpr  10987  ltexprlem3  10991  ltexprlem6  10994  ltapr  10998  prlem936  11000  suplem1pr  11005  axpre-sup  11122  1re  11174  dedekindle  11338  lemul12a  12040  divgt0  12051  divge0  12052  lbreu  12133  sup2  12139  bndndx  12441  elnnz  12539  nzadd  12581  fzind  12632  fnn0ind  12633  uzwo  12870  lbzbi  12895  zmax  12904  zbtwnre  12905  irradd  12932  irrmul  12933  ledivge1le  13024  xrub  13272  supxrunb2  13280  infmremnf  13304  iccid  13351  uzsubsubfz  13507  fzrevral  13573  elfz0fzfz0  13594  fz0fzelfz0  13595  elfzmlbp  13600  elincfzoext  13684  ssfzoulel  13721  ssfzo12bi  13722  fzoopth  13723  elfzonelfzo  13730  elfznelfzo  13733  elfznelfzob  13734  injresinjlem  13748  fleqceilz  13816  modaddmodup  13899  uzindi  13947  suppssfz  13959  mptnn0fsuppr  13964  le2sq2  14100  sqlecan  14174  facdiv  14252  facwordi  14254  faclbnd  14255  hashimarni  14406  hash2prd  14440  hashle2pr  14442  pr2pwpr  14444  fundmge2nop0  14467  fi1uzind  14472  brfi1indALT  14475  swrdnd2  14620  swrdnnn0nd  14621  swrdnd0  14622  pfxnd0  14653  swrdswrdlem  14669  swrdswrd  14670  ccatopth2  14682  wrd2ind  14688  pfxccatin12lem2a  14692  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12lem3  14697  swrdccat  14700  swrdccat3blem  14704  reuccatpfxs1lem  14711  repswswrd  14749  cshwidxmod  14768  cshwidx0  14771  2cshwcshw  14791  cshwcsh2id  14794  cau3lem  15321  caubnd  15325  climrlim2  15513  rlimcn3  15556  mulcn2  15562  climcau  15637  climbdd  15638  caucvg  15645  modfsummod  15760  p1modz1  16229  dvdsle  16280  dvdsdivcl  16286  ltoddhalfle  16331  halfleoddlt  16332  ndvdssub  16379  gcdcllem1  16469  dvdslegcd  16474  bezoutlem4  16512  dfgcd2  16516  lcmf  16603  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem  16611  lcmfdvdsb  16613  lcmfun  16615  coprmdvds1  16622  divgcdcoprm0  16635  cncongr1  16637  cncongr2  16638  prmfac1  16690  pcqcl  16827  dvdsprmpweqle  16857  oddprmdvds  16874  prmpwdvds  16875  infpnlem1  16881  prmgaplem5  17026  prmgaplem6  17027  prmgaplem7  17028  cshwshashlem1  17066  cictr  17767  initoeu2lem1  17976  initoeu2  17978  clatleglb  18477  lidrididd  18597  mulgaddcom  19030  mulginvcom  19031  cycsubm  19134  cyccom  19135  gsmsymgreqlem2  19361  symggen  19400  psgnunilem4  19427  sylow2blem3  19552  frgpnabllem1  19803  imasabl  19806  dprddisj2  19971  lmodfopnelem1  20804  lssssr  20860  lss1d  20869  lspsncv0  21056  rnglidlmcl  21126  rngqiprngimfo  21211  nzerooringczr  21390  pzriprnglem5  21395  pzriprnglem8  21398  znrrg  21475  mplcoe5lem  21946  cply1mul  22183  coe1fzgsumdlem  22190  gsummoncoe1  22195  evl1gsumdlem  22243  mamufacex  22283  dmatelnd  22383  scmataddcl  22403  scmatsubcl  22404  scmatmulcl  22405  smatvscl  22411  mavmulsolcl  22438  mdetdiagid  22487  cramerlem3  22576  pmatcoe1fsupp  22588  cpmatacl  22603  cpmatmcllem  22605  mp2pm2mplem4  22696  chpscmat  22729  chfacfisf  22741  chfacfisfcpmat  22742  uniopn  22784  opnnei  23007  neindisj2  23010  restcls  23068  restntr  23069  tgcnp  23140  subbascn  23141  iscnp4  23150  lpcls  23251  cmpsublem  23286  cmpsub  23287  tgcmp  23288  cmpcld  23289  dfconn2  23306  1stcrest  23340  2ndcdisj  23343  1stccnp  23349  comppfsc  23419  kgencn2  23444  txlm  23535  kqreglem1  23628  filin  23741  isfil2  23743  ufilmax  23794  ufileu  23806  filufint  23807  cfinufil  23815  elfm2  23835  rnelfmlem  23839  rnelfm  23840  flimopn  23862  fbflim2  23864  flffbas  23882  fclsnei  23906  flimfnfcls  23915  fclscmp  23917  fcfnei  23922  cnpfcf  23928  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  ptcmplem4  23942  qustgplem  24008  tsmsres  24031  tsmsxp  24042  metss  24396  metcnp3  24428  ovoliunnul  25408  ovolicc2lem3  25420  dyadmax  25499  itg2le  25640  bddiblnc  25743  itgcn  25746  ellimc3  25780  lhop1  25919  dvfsumrlim  25938  fta1g  26075  dvply2g  26192  fta1  26216  aalioulem3  26242  aalioulem4  26243  ulmcaulem  26303  ulmcau  26304  logbgcd1irr  26704  xrlimcnp  26878  cxploglim  26888  jensen  26899  lgsqrmodndvds  27264  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  lgsquad2lem2  27296  2lgslem1a1  27300  2sqlem6  27334  2sq2  27344  2sqnn  27350  2sqreultblem  27359  nosepdmlem  27595  nodenselem8  27603  madebdaylemlrcut  27810  addsprop  27883  addsuniflem  27908  negsprop  27941  mulsprop  28033  mulsuniflem  28052  precsex  28120  onsfi  28247  elnnzs  28289  brbtwn2  28832  ax5seglem5  28860  axcontlem4  28894  axcontlem10  28900  umgrnloopv  29033  umgrnloop  29035  upgredgpr  29069  numedglnl  29071  usgrausgrb  29096  usgrnloopvALT  29128  usgrnloopALT  29130  usgredg2vlem2  29153  ushgredgedg  29156  ushgredgedgloop  29158  upgrreslem  29231  umgrreslem  29232  nbgr0edglem  29283  nbusgrvtxm1  29306  uvtxnbgrvtx  29320  cusgredg  29351  cusgrres  29376  cusgrsize2inds  29381  cusgrfi  29386  fusgrregdegfi  29497  ewlkle  29533  uspgr2wlkeqi  29576  lfgrwlkprop  29615  lfgrwlknloop  29617  pthdivtx  29657  2pthnloop  29661  upgrwlkdvdelem  29666  upgrspthswlk  29668  usgr2wlkneq  29686  usgr2trlncl  29690  usgr2pthlem  29693  usgr2pth  29694  uspgrn2crct  29738  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0  29751  wlkiswwlks1  29797  wlkiswwlks2  29805  wlkiswwlksupgr2  29807  wwlksnred  29822  wwlksnext  29823  wwlksnextbi  29824  wwlksnextwrd  29827  wwlksnextinj  29829  wwlksnextproplem2  29840  wwlksnextproplem3  29841  wspthsnonn0vne  29847  wspn0  29854  2pthon3v  29873  umgrwwlks2on  29887  elwspths2on  29890  wpthswwlks2on  29891  clwwlk1loop  29917  clwwlkccatlem  29918  umgrclwwlkge2  29920  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem3  29930  clwlkclwwlkf1lem3  29935  clwlkclwwlkfo  29938  clwwisshclwwslemlem  29942  erclwwlkeqlen  29948  erclwwlksym  29950  clwwlkf  29976  clwwlknscsh  29991  erclwwlknsym  29999  clwwlknonex2lem2  30037  clwwlknonex2  30038  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eucrctshift  30172  3vfriswmgr  30207  1to2vfriswmgr  30208  1to3vfriswmgr  30209  n4cyclfrgr  30220  4cyclusnfrgr  30221  frgrnbnb  30222  frgrncvvdeqlem8  30235  frgrwopreg  30252  frgr2wwlk1  30258  frgr2wwlkeqm  30260  2clwwlk2clwwlklem  30275  numclwwlk1lem2fo  30287  wlkl0  30296  numclwlk2lem2f  30306  frgrreggt1  30322  frgrreg  30323  frgrregord013  30324  frgrregord13  30325  frgrogt3nreg  30326  eulplig  30414  nmoub3i  30702  ipasslem5  30764  htthlem  30846  ocin  31225  spansneleq  31499  spansnss  31500  elspansn4  31502  h1datomi  31510  nmopub2tALT  31838  nmfnleub2  31855  hstel2  32148  cvnbtwn  32215  spansncv2  32222  dmdmd  32229  dmdbr3  32234  dmdbr4  32235  dmdbr5  32237  mdsl0  32239  mdexchi  32264  cvexchlem  32297  atcv1  32309  atomli  32311  atcvatlem  32314  atcvat2i  32316  chirredi  32323  mdsymlem3  32334  mdsymlem4  32335  sumdmdii  32344  sumdmdlem  32347  cdj1i  32362  ssrelf  32543  f1o3d  32551  fisshasheq  35102  umgr2cycllem  35127  cvxpconn  35229  satfv0  35345  satfsschain  35351  satfrel  35354  satfdm  35356  satfv0fun  35358  sat1el2xp  35366  gonarlem  35381  goalrlem  35383  satffunlem1lem1  35389  satffunlem2lem1  35391  satffunlem2lem2  35393  satffun  35396  mrsubccat  35505  msubvrs  35547  fundmpss  35754  dfon2lem6  35776  dfon2lem8  35778  dfon2lem9  35779  dfon2  35780  wzel  35812  colinearxfr  36063  btwnconn1lem11  36085  lineintmo  36145  in-ax8  36212  ss-ax8  36213  trer  36304  elicc3  36305  finminlem  36306  nn0prpwlem  36310  fnessref  36345  neibastop2  36349  fgmin  36358  tailfb  36365  ordcmp  36435  ee7.2aOLD  36449  bj-cbvalimt  36627  bj-ceqsalt0  36872  bj-ceqsalt1  36873  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlpssretop  37352  fvineqsneu  37399  fvineqsneq  37400  wl-mo3t  37564  finixpnum  37599  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  ftc1anc  37695  fdc  37739  heibor1lem  37803  ghomco  37885  rngoueqz  37934  unichnidl  38025  dmncan1  38070  ax12indn  38936  lshpdisj  38980  lub0N  39182  glb0N  39186  leat2  39287  hlrelat2  39397  cvrexchlem  39413  cvratlem  39415  atcvrj0  39422  cvrat2  39423  snatpsubN  39744  linepsubN  39746  pmaple  39755  pmapsub  39762  elpaddn0  39794  paddasslem5  39818  trlval2  40157  cdlemn11pre  41204  dihord2pre  41219  mapdordlem2  41631  sn-sup2  42479  fsuppind  42578  pell1qrgap  42862  dford3lem1  43015  hbtlem5  43117  onexlimgt  43232  onsucf1olem  43259  omcl2  43322  tfsconcat0b  43335  ntrneiiso  44080  sbiota1  44423  19.41rg  44540  ee223  44624  or2expropbilem1  47033  funressnfv  47044  fcoresf1  47070  2reuimp  47116  f1oresf1o2  47292  zm1nn  47303  nltle2tri  47314  el1fzopredsuc  47326  modlt0b  47364  mod2addne  47365  elsetpreimafvssdm  47387  imasetpreimafvbijlemf1  47405  iccpartlt  47425  iccpartgt  47428  iccelpart  47434  icceuelpart  47437  iccpartnel  47439  fargshiftfo  47443  fargshiftfva  47444  lswn0  47445  ich2exprop  47472  prsprel  47488  sprsymrelfolem2  47494  sprsymrelfo  47498  poprelb  47525  reuopreuprim  47527  goldbachthlem2  47547  odz2prm2pw  47564  fmtnoprmfac1  47566  fmtnofac2lem  47569  prmdvdsfmtnof1lem2  47586  2pwp1prm  47590  sfprmdvdsmersenne  47604  lighneallem3  47608  requad01  47622  requad2  47624  even3prm2  47720  fppr2odd  47732  fpprwpprb  47741  gbegt5  47762  sbgoldbwt  47778  sbgoldbalt  47782  sbgoldbm  47785  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgblthelfgott  47816  tgoldbach  47818  isubgredg  47866  grimuhgr  47887  grimcnv  47888  grimco  47889  isuspgrim0  47894  isuspgrimlem  47895  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933  grimedg  47935  grtriprop  47940  cycl3grtri  47946  grimgrtri  47948  isubgr3stgrlem6  47970  uspgrlimlem3  47989  uspgrlimlem4  47990  grlimgrtrilem2  47994  grlicsym  48005  clnbgr3stgrgrlic  48011  gpgedg2ov  48057  gpgedg2iv  48058  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  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