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  2283  moexexlem  2651  ralrimdvva  3217  ceqsal1t  3482  ceqsalt  3483  spcimgft  3510  vtoclgft  3515  elabgtOLD  3626  reupick  4274  reusv3  5366  sbcop1  5457  propeqop  5478  pwssun  5542  wefrc  5644  ssrel  5758  ssrel2  5760  ssrelrel  5771  ssrelrn  5875  tz7.7  6388  ordtr2  6408  onmindif  6457  unizlim  6487  funssres  6585  f1ssf1  6858  fvmptt  7015  fveqdmss  7079  fvcofneq  7094  funsndifnop  7156  funfvima2  7238  isoini  7347  isopolem  7354  weniso  7365  f1ocnv2d  7675  limsssuc  7862  tfindsg  7873  limomss  7883  findsg  7910  funcnvuni  7945  f1oweALT  7985  funelss  8059  bropopvvv  8102  bropfvvvvlem  8103  bropfvvvv  8104  f1o2ndf1  8136  frxp  8141  soseq  8179  suppfnss  8210  onfununi  8353  tz7.48lem  8454  tz7.49  8459  omordi  8578  omlimcl  8590  omass  8592  oeordsuc  8607  nnmordi  8644  nnmord  8645  omabs  8664  xpdom2  9095  infensuc  9178  findcard2  9184  findcard2d  9186  findcard3  9278  frfi  9280  fsuppres  9389  dffi2  9419  elfiun  9426  ordiso2  9513  ordtypelem7  9522  suc11reg  9624  inf3lem2  9634  noinfep  9665  cantnfle  9676  cantnflem1  9694  cantnf  9698  ttrclss  9725  trcl  9733  epfrs  9736  frr3g  9764  r1sdom  9785  setrec1lem2  9971  updjud  10019  dfac8alem  10112  indcardi  10124  alephordi  10157  dfac12lem3  10228  pwsdompw  10285  cofsmo  10351  cfcoflem  10354  coftr  10355  isf32lem2  10436  isf32lem9  10443  axcc3  10520  domtriomlem  10524  axdc3lem2  10533  axdc3lem4  10535  zorn2lem4  10581  zorn2lem6  10583  zorn2lem7  10584  ttukeylem6  10596  uniimadom  10632  konigthlem  10657  fpwwe2lem7  10726  tskord  10869  tskcard  10870  grupr  10886  gruiin  10899  grudomon  10906  grur1a  10908  genpn0  11092  genpcd  11095  distrlem5pr  11116  psslinpr  11120  ltaddpr  11123  ltexprlem3  11127  ltexprlem6  11130  ltapr  11134  prlem936  11136  suplem1pr  11141  axpre-sup  11258  1re  11312  dedekindle  11478  lemul12a  12179  divgt0  12189  divge0  12190  lbreu  12271  sup2  12277  bndndx  12609  elnnz  12707  nzadd  12748  fzind  12801  fnn0ind  12802  uzwo  13042  lbzbi  13067  zmax  13076  zbtwnre  13077  irradd  13105  irrmul  13106  ledivge1le  13197  xrub  13446  supxrunb2  13454  infmremnf  13478  iccid  13525  uzsubsubfz  13684  fzrevral  13750  elfz0fzfz0  13771  fz0fzelfz0  13772  elfzmlbp  13777  elincfzoext  13862  ssfzoulel  13899  ssfzo12bi  13900  fzoopth  13901  elfzonelfzo  13908  elfznelfzo  13912  elfznelfzob  13913  injresinjlem  13929  fleqceilz  13998  modaddmodup  14081  uzindi  14129  suppssfz  14141  mptnn0fsuppr  14146  le2sq2  14282  sqlecan  14357  facdiv  14435  facwordi  14437  faclbnd  14438  hashimarni  14590  hash2prd  14624  hashle2pr  14626  pr2pwpr  14628  fundmge2nop0  14651  fi1uzind  14656  brfi1indALT  14659  swrdnd2  14810  swrdnnn0nd  14811  swrdnd0  14812  pfxnd0  14843  swrdswrdlem  14858  swrdswrd  14859  ccatopth2  14871  wrd2ind  14877  pfxccatin12lem2a  14881  swrdccatin2  14883  pfxccatin12lem2  14885  pfxccatin12lem3  14886  swrdccat  14889  swrdccat3blem  14893  reuccatpfxs1lem  14900  repswswrd  14940  cshwidxmod  14959  cshwidx0  14962  2cshwcshw  14981  cshwcsh2id  14984  cau3lem  15528  caubnd  15532  climrlim2  15720  rlimcn3  15763  mulcn2  15769  climcau  15844  climbdd  15845  caucvg  15852  modfsummod  15967  p1modz1  16435  dvdsle  16486  dvdsdivcl  16492  ltoddhalfle  16537  halfleoddlt  16538  ndvdssub  16585  gcdcllem1  16675  dvdslegcd  16680  bezoutlem4  16721  dfgcd2  16725  lcmf  16814  lcmfunsnlem1  16818  lcmfunsnlem2lem1  16819  lcmfunsnlem  16822  lcmfdvdsb  16824  lcmfun  16826  coprmdvds1  16833  divgcdcoprm0  16846  cncongr1  16848  cncongr2  16849  prmfac1  16902  pcqcl  17040  dvdsprmpweqle  17070  oddprmdvds  17087  prmpwdvds  17088  infpnlem1  17094  prmgaplem5  17239  prmgaplem6  17240  prmgaplem7  17241  cshwshashlem1  17279  cictr  17986  initoeu2lem1  18195  initoeu2  18197  clatleglb  18698  lidrididd  18857  mulgaddcom  19314  mulginvcom  19315  cycsubm  19423  cyccom  19424  gsmsymgreqlem2  19651  symggen  19690  psgnunilem4  19717  sylow2blem3  19842  frgpnabllem1  20093  imasabl  20096  dprddisj2  20261  lmodfopnelem1  21179  lssssr  21235  lss1d  21244  lspsncv0  21430  rnglidlmcl  21501  lidlunin0  21521  unichnlidl  21522  rngqiprngimfo  21603  nzerooringczr  21792  pzriprnglem5  21797  pzriprnglem8  21800  znrrg  21877  mplcoe5lem  22354  cply1mul  22620  coe1fzgsumdlem  22627  gsummoncoe1  22632  evl1gsumdlem  22680  mamufacex  22717  dmatelnd  22817  scmataddcl  22837  scmatsubcl  22838  scmatmulcl  22839  smatvscl  22845  mavmulsolcl  22872  mdetdiagid  22921  matunitlindflem1  23000  matunitlindflem2  23001  cramerlem3  23013  pmatcoe1fsupp  23025  cpmatacl  23040  cpmatmcllem  23042  mp2pm2mplem4  23133  chpscmat  23166  chfacfisf  23178  chfacfisfcpmat  23179  uniopn  23221  opnnei  23444  neindisj2  23447  restcls  23505  restntr  23506  tgcnp  23577  subbascn  23578  iscnp4  23587  lpcls  23688  cmpsublem  23723  cmpsub  23724  tgcmp  23725  cmpcld  23726  dfconn2  23743  1stcrest  23777  2ndcdisj  23781  1stccnp  23787  comppfsc  23857  kgencn2  23882  txlm  23973  kqreglem1  24066  filin  24179  isfil2  24181  ufilmax  24232  ufileu  24244  filufint  24245  cfinufil  24253  elfm2  24273  rnelfmlem  24277  rnelfm  24278  flimopn  24300  fbflim2  24302  flffbas  24320  fclsnei  24344  flimfnfcls  24353  fclscmp  24355  fcfnei  24360  cnpfcf  24366  alexsubALTlem2  24373  alexsubALTlem3  24374  alexsubALTlem4  24375  alexsubALT  24376  ptcmplem4  24380  qustgplem  24446  tsmsres  24469  tsmsxp  24480  metss  24833  metcnp3  24865  ovoliunnul  25834  ovolicc2lem3  25846  dyadmax  25925  itg2le  26066  bddiblnc  26168  itgcn  26171  ellimc3  26205  lhop1  26340  dvfsumrlim  26357  fta1g  26494  dvply2g  26612  fta1  26635  aalioulem3  26667  aalioulem4  26668  ulmcaulem  26727  ulmcau  26728  logbgcd1irr  27128  xrlimcnp  27302  cxploglim  27311  jensen  27322  lgsqrmodndvds  27686  gausslemma2dlem1a  27698  gausslemma2dlem2  27700  gausslemma2dlem3  27701  lgsquad2lem2  27718  2lgslem1a1  27722  2sqlem6  27756  2sq2  27766  2sqnn  27772  2sqreultblem  27781  fltoprm  28001  fltoprmgt3  28002  nosepdmlem  28046  nodenselem8  28054  eqcuts3  28196  madebdaylemlrcut  28291  addsprop  28368  addsuniflem  28393  negsprop  28427  mulsprop  28522  mulsuniflem  28541  precsex  28610  onsfi  28748  elnnzs  28793  elreno2  28887  brbtwn2  29489  ax5seglem5  29517  axcontlem4  29551  axcontlem10  29557  umgrnloopv  29690  umgrnloop  29692  upgredgpr  29726  numedglnl  29728  usgrausgrb  29756  usgrnloopvALT  29788  usgrnloopALT  29790  usgredg2vlem2  29813  ushgredgedg  29816  ushgredgedgloop  29818  upgrreslem  29891  umgrreslem  29892  nbgr0edglem  29943  nbusgrvtxm1  29966  uvtxnbgrvtx  29980  cusgredg  30011  cusgrres  30035  cusgrsize2inds  30040  cusgrfi  30045  fusgrregdegfi  30156  ewlkle  30192  uspgr2wlkeqi  30234  lfgrwlkprop  30276  lfgrwlknloop  30278  pthdivtx  30318  2pthnloop  30323  upgrwlkdvdelem  30328  upgrspthswlk  30330  usgr2wlkneq  30348  usgr2trlncl  30352  usgr2pthlem  30355  usgr2pth  30356  uspgrn2crct  30403  crctcshwlkn0lem4  30408  crctcshwlkn0lem5  30409  crctcshwlkn0  30416  wlkiswwlks1  30462  wlkiswwlks2  30470  wlkiswwlksupgr2  30472  wwlksnred  30487  wwlksnext  30488  wwlksnextbi  30489  wwlksnextwrd  30492  wwlksnextinj  30494  wwlksnextproplem2  30505  wwlksnextproplem3  30506  wspthsnonn0vne  30512  wspn0  30519  2pthon3v  30538  usgrwwlks2on  30553  umgrwwlks2on  30554  elwspths2on  30557  elwspths2onw  30558  wpthswwlks2on  30559  clwwlk1loop  30585  clwwlkccatlem  30586  umgrclwwlkge2  30588  clwlkclwwlklem2a4  30594  clwlkclwwlklem2a  30595  clwlkclwwlklem3  30598  clwlkclwwlkf1lem3  30603  clwlkclwwlkfo  30606  clwwisshclwwslemlem  30610  erclwwlkeqlen  30616  erclwwlksym  30618  clwwlkf  30644  clwwlknscsh  30659  erclwwlknsym  30667  clwwlknonex2lem2  30705  clwwlknonex2  30706  umgr2cycllem  30752  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  eucrctshift  30850  3vfriswmgr  30885  1to2vfriswmgr  30886  1to3vfriswmgr  30887  n4cyclfrgr  30898  4cyclusnfrgr  30899  frgrnbnb  30900  frgrncvvdeqlem8  30913  frgrwopreg  30930  frgr2wwlk1  30936  frgr2wwlkeqm  30938  2clwwlk2clwwlklem  30953  numclwwlk1lem2fo  30965  wlkl0  30974  numclwlk2lem2f  30984  frgrreggt1  31000  frgrreg  31001  frgrregord013  31002  frgrregord13  31003  frgrogt3nreg  31004  eulplig  31093  nmoub3i  31381  ipasslem5  31443  htthlem  31525  ocin  31904  spansneleq  32178  spansnss  32179  elspansn4  32181  h1datomi  32189  nmopub2tALT  32517  nmfnleub2  32534  hstel2  32827  cvnbtwn  32894  spansncv2  32901  dmdmd  32908  dmdbr3  32913  dmdbr4  32914  dmdbr5  32916  mdsl0  32918  mdexchi  32943  cvexchlem  32976  atcv1  32988  atomli  32990  atcvatlem  32993  atcvat2i  32995  chirredi  33002  mdsymlem3  33013  mdsymlem4  33014  sumdmdii  33023  sumdmdlem  33026  cdj1i  33041  ssrelf  33257  f1o3d  33268  onprcf1acwevdlem1  35965  fisshasheq  35980  cvxpconn  36094  satfv0  36210  satfsschain  36216  satfrel  36219  satfdm  36221  satfv0fun  36223  sat1el2xp  36231  gonarlem  36246  goalrlem  36248  satffunlem1lem1  36254  satffunlem2lem1  36256  satffunlem2lem2  36258  satffun  36261  mrsubccat  36370  msubvrs  36412  fundmpss  36625  dfon2lem6  36643  dfon2lem8  36645  dfon2lem9  36646  dfon2  36647  wzel  36679  colinearxfr  36933  btwnconn1lem11  36955  lineintmo  37015  in-ax8  37106  ss-ax8  37107  trer  37197  elicc3  37198  finminlem  37199  nn0prpwlem  37203  fnessref  37238  neibastop2  37242  fgmin  37251  tailfb  37258  ordcmp  37328  ee7.2aOLD  37342  dfttc4  37411  bj-ceqsalt0  37889  bj-ceqsalt1  37890  isbasisrelowllem1  38372  isbasisrelowllem2  38373  relowlpssretop  38381  fvineqsneu  38428  fvineqsneq  38429  wl-mo3t  38602  finixpnum  38622  poimirlem26  38658  poimirlem27  38659  poimirlem29  38661  ftc1anc  38713  fdc  38773  heibor1lem  38837  ghomco  38919  rngoueqz  38968  unichnidl  39059  dmncan1  39104  ax12indn  40094  lshpdisj  40138  lub0N  40340  glb0N  40344  leat2  40445  hlrelat2  40554  cvrexchlem  40570  cvratlem  40572  atcvrj0  40579  cvrat2  40580  snatpsubN  40901  linepsubN  40903  pmaple  40912  pmapsub  40919  elpaddn0  40951  paddasslem5  40975  trlval2  41314  cdlemn11pre  42361  dihord2pre  42376  mapdordlem2  42788  sn-sup2  43649  fsuppind  43712  pell1qrgap  43975  dford3lem1  44127  hbtlem5  44224  onexlimgt  44339  onsucf1olem  44366  omcl2  44429  tfsconcat0b  44442  ntrneiiso  45185  sbiota1  45512  19.41rg  45627  ee223  45711  cocanss2  46016  or2expropbilem1  48196  funressnfv  48207  fcoresf1  48233  2reuimp  48279  f1oresf1o2  48455  zm1nn  48466  nltle2tri  48477  el1fzopredsuc  48490  modlt0b  48533  mod2addne  48534  muldvdsfacgt  48550  muldvdsfacm1  48551  elsetpreimafvssdm  48562  imasetpreimafvbijlemf1  48580  iccpartlt  48600  iccpartgt  48603  iccelpart  48609  icceuelpart  48612  iccpartnel  48614  fargshiftfo  48618  fargshiftfva  48619  lswn0  48620  ich2exprop  48647  prsprel  48663  sprsymrelfolem2  48669  sprsymrelfo  48673  poprelb  48700  reuopreuprim  48702  goldbachthlem2  48725  odz2prm2pw  48742  fmtnoprmfac1  48744  fmtnofac2lem  48747  prmdvdsfmtnof1lem2  48764  2pwp1prm  48768  sfprmdvdsmersenne  48782  lighneallem3  48786  requad01  48813  requad2  48815  even3prm2  48911  fppr2odd  48923  fpprwpprb  48932  gbegt5  48953  sbgoldbwt  48969  sbgoldbalt  48973  sbgoldbm  48976  bgoldbtbndlem2  48998  bgoldbtbndlem3  48999  bgoldbtbndlem4  49000  bgoldbtbnd  49001  tgblthelfgott  49007  tgoldbach  49009  isubgredg  49058  grimuhgr  49079  grimcnv  49080  grimco  49081  isuspgrim0  49086  isuspgrimlem  49087  uhgrimisgrgriclem  49122  clnbgrgrimlem  49125  grimedg  49127  grtriprop  49133  cycl3grtri  49139  grimgrtri  49141  isubgr3stgrlem6  49163  uspgrlimlem3  49182  uspgrlimlem4  49183  grlimgrtrilem2  49194  grlicsym  49205  clnbgr3stgrgrlim  49211  clnbgr3stgrgrlic  49212  gpgedg2ov  49258  gpgedg2iv  49259  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem6  49316  upgrwlkupwlk  49332  lmod0rng  49420  idomcanl  49538  ztprmneprm  49553  ply1mulgsumlem1  49592  ply1mulgsumlem2  49593  lcoel0  49634  linindslinci  49654  lindslinindimp2lem4  49667  lindslinindsimp2lem5  49668  snlindsntor  49677  ldepspr  49679  lincresunit2  49684  fllog2  49774  dignn0ldlem  49808  dignn0flhalflem1  49821  nn0sumshdiglemA  49825  nn0sumshdiglemB  49826  itcovalt2  49883  resum2sqorgt0  49915  eenglngeehlnmlem2  49945  rrx2linest  49948  itscnhlc0xyqsol  49971  itsclc0  49977  aacllem  51108