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  2286  moexexlem  2656  ralrimdvva  3222  ceqsal1t  3489  ceqsalt  3490  spcimgft  3517  vtoclgft  3522  elabgtOLD  3634  reupick  4282  reusv3  5378  sbcop1  5472  propeqop  5492  pwssun  5555  wefrc  5657  ssrel  5771  ssrel2  5773  ssrelrel  5784  ssrelrn  5886  tz7.7  6390  ordtr2  6410  onmindif  6459  unizlim  6489  funssres  6584  f1ssf1  6857  fvmptt  7014  fveqdmss  7077  fvcofneq  7092  funsndifnop  7152  funfvima2  7233  isoini  7342  isopolem  7349  weniso  7360  f1ocnv2d  7669  limsssuc  7848  tfindsg  7859  limomss  7869  findsg  7896  funcnvuni  7931  f1oweALT  7971  funelss  8046  bropopvvv  8087  bropfvvvvlem  8088  bropfvvvv  8089  f1o2ndf1  8119  frxp  8124  soseq  8157  suppfnss  8187  onfununi  8330  tz7.49  8434  omordi  8553  omlimcl  8565  omass  8567  oeordsuc  8582  nnmordi  8619  nnmord  8620  omabs  8639  xpdom2  9063  infensuc  9146  findcard2  9152  findcard2d  9154  findcard3  9246  frfi  9248  fsuppres  9356  dffi2  9386  elfiun  9393  ordiso2  9480  ordtypelem7  9489  suc11reg  9591  inf3lem2  9601  noinfep  9632  cantnfle  9643  cantnflem1  9661  cantnf  9665  ttrclss  9692  trcl  9700  epfrs  9703  frr3g  9731  r1sdom  9749  updjud  9932  dfac8alem  10025  indcardi  10037  alephordi  10070  dfac12lem3  10141  pwsdompw  10198  cofsmo  10264  cfcoflem  10267  coftr  10268  isf32lem2  10349  isf32lem9  10356  axcc3  10433  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  zorn2lem4  10494  zorn2lem6  10496  zorn2lem7  10497  ttukeylem6  10509  uniimadom  10539  konigthlem  10564  fpwwe2lem7  10633  tskord  10776  tskcard  10777  grupr  10793  gruiin  10806  grudomon  10813  grur1a  10815  genpn0  10999  genpcd  11002  distrlem5pr  11023  psslinpr  11027  ltaddpr  11030  ltexprlem3  11034  ltexprlem6  11037  ltapr  11041  prlem936  11043  suplem1pr  11048  axpre-sup  11165  1re  11219  dedekindle  11385  lemul12a  12084  divgt0  12094  divge0  12095  lbreu  12176  sup2  12182  bndndx  12514  elnnz  12612  nzadd  12653  fzind  12706  fnn0ind  12707  uzwo  12947  lbzbi  12972  zmax  12981  zbtwnre  12982  irradd  13009  irrmul  13010  ledivge1le  13101  xrub  13350  supxrunb2  13358  infmremnf  13382  iccid  13429  uzsubsubfz  13587  fzrevral  13653  elfz0fzfz0  13674  fz0fzelfz0  13675  elfzmlbp  13680  elincfzoext  13765  ssfzoulel  13802  ssfzo12bi  13803  fzoopth  13804  elfzonelfzo  13811  elfznelfzo  13815  elfznelfzob  13816  injresinjlem  13832  fleqceilz  13901  modaddmodup  13984  uzindi  14032  suppssfz  14044  mptnn0fsuppr  14049  le2sq2  14185  sqlecan  14259  facdiv  14337  facwordi  14339  faclbnd  14340  hashimarni  14492  hash2prd  14526  hashle2pr  14528  pr2pwpr  14530  fundmge2nop0  14553  fi1uzind  14558  brfi1indALT  14561  swrdnd2  14711  swrdnnn0nd  14712  swrdnd0  14713  pfxnd0  14744  swrdswrdlem  14759  swrdswrd  14760  ccatopth2  14772  wrd2ind  14778  pfxccatin12lem2a  14782  swrdccatin2  14784  pfxccatin12lem2  14786  pfxccatin12lem3  14787  swrdccat  14790  swrdccat3blem  14794  reuccatpfxs1lem  14801  repswswrd  14841  cshwidxmod  14860  cshwidx0  14863  2cshwcshw  14882  cshwcsh2id  14885  cau3lem  15426  caubnd  15430  climrlim2  15618  rlimcn3  15661  mulcn2  15667  climcau  15742  climbdd  15743  caucvg  15750  modfsummod  15865  p1modz1  16335  dvdsle  16386  dvdsdivcl  16392  ltoddhalfle  16437  halfleoddlt  16438  ndvdssub  16485  gcdcllem1  16575  dvdslegcd  16580  bezoutlem4  16618  dfgcd2  16622  lcmf  16709  lcmfunsnlem1  16713  lcmfunsnlem2lem1  16714  lcmfunsnlem  16717  lcmfdvdsb  16719  lcmfun  16721  coprmdvds1  16728  divgcdcoprm0  16741  cncongr1  16743  cncongr2  16744  prmfac1  16797  pcqcl  16934  dvdsprmpweqle  16964  oddprmdvds  16981  prmpwdvds  16982  infpnlem1  16988  prmgaplem5  17133  prmgaplem6  17134  prmgaplem7  17135  cshwshashlem1  17173  cictr  17880  initoeu2lem1  18089  initoeu2  18091  clatleglb  18592  lidrididd  18747  mulgaddcom  19188  mulginvcom  19189  cycsubm  19297  cyccom  19298  gsmsymgreqlem2  19525  symggen  19564  psgnunilem4  19591  sylow2blem3  19716  frgpnabllem1  19967  imasabl  19970  dprddisj2  20135  lmodfopnelem1  21049  lssssr  21105  lss1d  21114  lspsncv0  21300  rnglidlmcl  21371  lidlunin0  21391  unichnlidl  21392  rngqiprngimfo  21471  nzerooringczr  21660  pzriprnglem5  21665  pzriprnglem8  21668  znrrg  21745  mplcoe5lem  22220  cply1mul  22486  coe1fzgsumdlem  22493  gsummoncoe1  22498  evl1gsumdlem  22546  mamufacex  22583  dmatelnd  22683  scmataddcl  22703  scmatsubcl  22704  scmatmulcl  22705  smatvscl  22711  mavmulsolcl  22738  mdetdiagid  22787  cramerlem3  22876  pmatcoe1fsupp  22888  cpmatacl  22903  cpmatmcllem  22905  mp2pm2mplem4  22996  chpscmat  23029  chfacfisf  23041  chfacfisfcpmat  23042  uniopn  23084  opnnei  23307  neindisj2  23310  restcls  23368  restntr  23369  tgcnp  23440  subbascn  23441  iscnp4  23450  lpcls  23551  cmpsublem  23586  cmpsub  23587  tgcmp  23588  cmpcld  23589  dfconn2  23606  1stcrest  23640  2ndcdisj  23644  1stccnp  23650  comppfsc  23720  kgencn2  23745  txlm  23836  kqreglem1  23929  filin  24042  isfil2  24044  ufilmax  24095  ufileu  24107  filufint  24108  cfinufil  24116  elfm2  24136  rnelfmlem  24140  rnelfm  24141  flimopn  24163  fbflim2  24165  flffbas  24183  fclsnei  24207  flimfnfcls  24216  fclscmp  24218  fcfnei  24223  cnpfcf  24229  alexsubALTlem2  24236  alexsubALTlem3  24237  alexsubALTlem4  24238  alexsubALT  24239  ptcmplem4  24243  qustgplem  24309  tsmsres  24332  tsmsxp  24343  metss  24696  metcnp3  24728  ovoliunnul  25697  ovolicc2lem3  25709  dyadmax  25788  itg2le  25929  bddiblnc  26032  itgcn  26035  ellimc3  26069  lhop1  26204  dvfsumrlim  26221  fta1g  26358  dvply2g  26477  fta1  26500  aalioulem3  26528  aalioulem4  26529  ulmcaulem  26588  ulmcau  26589  logbgcd1irr  26990  xrlimcnp  27164  cxploglim  27173  jensen  27184  lgsqrmodndvds  27548  gausslemma2dlem1a  27560  gausslemma2dlem2  27562  gausslemma2dlem3  27563  lgsquad2lem2  27580  2lgslem1a1  27584  2sqlem6  27618  2sq2  27628  2sqnn  27634  2sqreultblem  27643  nosepdmlem  27878  nodenselem8  27886  eqcuts3  28028  madebdaylemlrcut  28123  addsprop  28200  addsuniflem  28225  negsprop  28259  mulsprop  28354  mulsuniflem  28373  precsex  28442  onsfi  28580  elnnzs  28625  elreno2  28719  brbtwn2  29286  ax5seglem5  29314  axcontlem4  29348  axcontlem10  29354  umgrnloopv  29487  umgrnloop  29489  upgredgpr  29523  numedglnl  29525  usgrausgrb  29553  usgrnloopvALT  29585  usgrnloopALT  29587  usgredg2vlem2  29610  ushgredgedg  29613  ushgredgedgloop  29615  upgrreslem  29688  umgrreslem  29689  nbgr0edglem  29740  nbusgrvtxm1  29763  uvtxnbgrvtx  29777  cusgredg  29808  cusgrres  29832  cusgrsize2inds  29837  cusgrfi  29842  fusgrregdegfi  29953  ewlkle  29989  uspgr2wlkeqi  30031  lfgrwlkprop  30073  lfgrwlknloop  30075  pthdivtx  30115  2pthnloop  30120  upgrwlkdvdelem  30125  upgrspthswlk  30127  usgr2wlkneq  30145  usgr2trlncl  30149  usgr2pthlem  30152  usgr2pth  30153  uspgrn2crct  30200  crctcshwlkn0lem4  30205  crctcshwlkn0lem5  30206  crctcshwlkn0  30213  wlkiswwlks1  30259  wlkiswwlks2  30267  wlkiswwlksupgr2  30269  wwlksnred  30284  wwlksnext  30285  wwlksnextbi  30286  wwlksnextwrd  30289  wwlksnextinj  30291  wwlksnextproplem2  30302  wwlksnextproplem3  30303  wspthsnonn0vne  30309  wspn0  30316  2pthon3v  30335  usgrwwlks2on  30350  umgrwwlks2on  30351  elwspths2on  30354  elwspths2onw  30355  wpthswwlks2on  30356  clwwlk1loop  30382  clwwlkccatlem  30383  umgrclwwlkge2  30385  clwlkclwwlklem2a4  30391  clwlkclwwlklem2a  30392  clwlkclwwlklem3  30395  clwlkclwwlkf1lem3  30400  clwlkclwwlkfo  30403  clwwisshclwwslemlem  30407  erclwwlkeqlen  30413  erclwwlksym  30415  clwwlkf  30441  clwwlknscsh  30456  erclwwlknsym  30464  clwwlknonex2lem2  30502  clwwlknonex2  30503  umgr2cycllem  30549  upgr3v3e3cycl  30578  upgr4cycl4dv4e  30583  eucrctshift  30641  3vfriswmgr  30676  1to2vfriswmgr  30677  1to3vfriswmgr  30678  n4cyclfrgr  30689  4cyclusnfrgr  30690  frgrnbnb  30691  frgrncvvdeqlem8  30704  frgrwopreg  30721  frgr2wwlk1  30727  frgr2wwlkeqm  30729  2clwwlk2clwwlklem  30744  numclwwlk1lem2fo  30756  wlkl0  30765  numclwlk2lem2f  30775  frgrreggt1  30791  frgrreg  30792  frgrregord013  30793  frgrregord13  30794  frgrogt3nreg  30795  eulplig  30884  nmoub3i  31172  ipasslem5  31234  htthlem  31316  ocin  31695  spansneleq  31969  spansnss  31970  elspansn4  31972  h1datomi  31980  nmopub2tALT  32308  nmfnleub2  32325  hstel2  32618  cvnbtwn  32685  spansncv2  32692  dmdmd  32699  dmdbr3  32704  dmdbr4  32705  dmdbr5  32707  mdsl0  32709  mdexchi  32734  cvexchlem  32767  atcv1  32779  atomli  32781  atcvatlem  32784  atcvat2i  32786  chirredi  32793  mdsymlem3  32804  mdsymlem4  32805  sumdmdii  32814  sumdmdlem  32817  cdj1i  32832  ssrelf  33007  f1o3d  33018  fisshasheq  35637  cvxpconn  35747  satfv0  35863  satfsschain  35869  satfrel  35872  satfdm  35874  satfv0fun  35876  sat1el2xp  35884  gonarlem  35899  goalrlem  35901  satffunlem1lem1  35907  satffunlem2lem1  35909  satffunlem2lem2  35911  satffun  35914  mrsubccat  36023  msubvrs  36065  fundmpss  36272  dfon2lem6  36291  dfon2lem8  36293  dfon2lem9  36294  dfon2  36295  wzel  36327  colinearxfr  36580  btwnconn1lem11  36602  lineintmo  36662  in-ax8  36769  ss-ax8  36770  trer  36860  elicc3  36861  finminlem  36862  nn0prpwlem  36866  fnessref  36901  neibastop2  36905  fgmin  36914  tailfb  36921  ordcmp  36991  ee7.2aOLD  37005  dfttc4  37074  bj-ceqsalt0  37552  bj-ceqsalt1  37553  isbasisrelowllem1  38034  isbasisrelowllem2  38035  relowlpssretop  38043  fvineqsneu  38090  fvineqsneq  38091  wl-mo3t  38264  finixpnum  38289  matunitlindflem1  38300  matunitlindflem2  38301  poimirlem26  38330  poimirlem27  38331  poimirlem29  38333  ftc1anc  38385  fdc  38429  heibor1lem  38493  ghomco  38575  rngoueqz  38624  unichnidl  38715  dmncan1  38760  ax12indn  39750  lshpdisj  39794  lub0N  39996  glb0N  40000  leat2  40101  hlrelat2  40210  cvrexchlem  40226  cvratlem  40228  atcvrj0  40235  cvrat2  40236  snatpsubN  40557  linepsubN  40559  pmaple  40568  pmapsub  40575  elpaddn0  40607  paddasslem5  40631  trlval2  40970  cdlemn11pre  42017  dihord2pre  42032  mapdordlem2  42444  sn-sup2  43298  fsuppind  43355  pell1qrgap  43634  dford3lem1  43786  hbtlem5  43888  onexlimgt  44003  onsucf1olem  44030  omcl2  44093  tfsconcat0b  44106  ntrneiiso  44850  sbiota1  45177  19.41rg  45292  ee223  45376  or2expropbilem1  47802  funressnfv  47813  fcoresf1  47839  2reuimp  47885  f1oresf1o2  48061  zm1nn  48072  nltle2tri  48083  el1fzopredsuc  48096  modlt0b  48139  mod2addne  48140  muldvdsfacgt  48156  muldvdsfacm1  48157  elsetpreimafvssdm  48168  imasetpreimafvbijlemf1  48186  iccpartlt  48206  iccpartgt  48209  iccelpart  48215  icceuelpart  48218  iccpartnel  48220  fargshiftfo  48224  fargshiftfva  48225  lswn0  48226  ich2exprop  48253  prsprel  48269  sprsymrelfolem2  48275  sprsymrelfo  48279  poprelb  48306  reuopreuprim  48308  goldbachthlem2  48331  odz2prm2pw  48348  fmtnoprmfac1  48350  fmtnofac2lem  48353  prmdvdsfmtnof1lem2  48370  2pwp1prm  48374  sfprmdvdsmersenne  48388  lighneallem3  48392  requad01  48419  requad2  48421  even3prm2  48517  fppr2odd  48529  fpprwpprb  48538  gbegt5  48559  sbgoldbwt  48575  sbgoldbalt  48579  sbgoldbm  48582  bgoldbtbndlem2  48604  bgoldbtbndlem3  48605  bgoldbtbndlem4  48606  bgoldbtbnd  48607  tgblthelfgott  48613  tgoldbach  48615  isubgredg  48664  grimuhgr  48685  grimcnv  48686  grimco  48687  isuspgrim0  48692  isuspgrimlem  48693  uhgrimisgrgriclem  48728  clnbgrgrimlem  48731  grimedg  48733  grtriprop  48739  cycl3grtri  48745  grimgrtri  48747  isubgr3stgrlem6  48769  uspgrlimlem3  48788  uspgrlimlem4  48789  grlimgrtrilem2  48800  grlicsym  48811  clnbgr3stgrgrlim  48817  clnbgr3stgrgrlic  48818  gpgedg2ov  48864  gpgedg2iv  48865  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem6  48922  upgrwlkupwlk  48938  lmod0rng  49027  idomcanl  49145  ztprmneprm  49160  ply1mulgsumlem1  49199  ply1mulgsumlem2  49200  lcoel0  49241  linindslinci  49261  lindslinindimp2lem4  49274  lindslinindsimp2lem5  49275  snlindsntor  49284  ldepspr  49286  lincresunit2  49291  fllog2  49381  dignn0ldlem  49415  dignn0flhalflem1  49428  nn0sumshdiglemA  49432  nn0sumshdiglemB  49433  itcovalt2  49490  resum2sqorgt0  49522  eenglngeehlnmlem2  49551  rrx2linest  49555  itscnhlc0xyqsol  49578  itsclc0  49584  setrec1lem2  50499  aacllem  50654