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  2251  moexexlem  2621  ralrimdvva  3187  ceqsal1t  3469  ceqsalt  3470  spcimgft  3501  vtoclgft  3507  elabgtOLD  3628  sbciegftOLD  3779  reupick  4279  reusv3  5343  sbcop1  5428  propeqop  5447  pwssun  5508  wefrc  5610  ssrel  5723  ssrel2  5725  ssrelrel  5736  ssrelrn  5834  tz7.7  6332  ordtr2  6351  onmindif  6400  unizlim  6430  funssres  6525  f1ssf1  6795  fvmptt  6949  fveqdmss  7011  fvcofneq  7026  funsndifnop  7084  funfvima2  7165  isoini  7272  isopolem  7279  weniso  7288  f1ocnv2d  7599  limsssuc  7780  tfindsg  7791  limomss  7801  findsg  7827  funcnvuni  7862  f1oweALT  7904  funelss  7979  bropopvvv  8020  bropfvvvvlem  8021  bropfvvvv  8022  f1o2ndf1  8052  frxp  8056  soseq  8089  suppfnss  8119  onfununi  8261  tz7.49  8364  omordi  8481  omlimcl  8493  omass  8495  oeordsuc  8509  nnmordi  8546  nnmord  8547  omabs  8566  xpdom2  8985  infensuc  9068  findcard2  9074  findcard2d  9076  findcard3  9167  frfi  9169  fsuppres  9277  dffi2  9307  elfiun  9314  ordiso2  9401  ordtypelem7  9410  suc11reg  9509  inf3lem2  9519  noinfep  9550  cantnfle  9561  cantnflem1  9579  cantnf  9583  ttrclss  9610  trcl  9618  epfrs  9621  frr3g  9649  r1sdom  9667  updjud  9827  dfac8alem  9920  indcardi  9932  alephordi  9965  dfac12lem3  10037  pwsdompw  10094  cofsmo  10160  cfcoflem  10163  coftr  10164  isf32lem2  10245  isf32lem9  10252  axcc3  10329  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  zorn2lem4  10390  zorn2lem6  10392  zorn2lem7  10393  ttukeylem6  10405  uniimadom  10435  konigthlem  10459  fpwwe2lem7  10528  tskord  10671  tskcard  10672  grupr  10688  gruiin  10701  grudomon  10708  grur1a  10710  genpn0  10894  genpcd  10897  distrlem5pr  10918  psslinpr  10922  ltaddpr  10925  ltexprlem3  10929  ltexprlem6  10932  ltapr  10936  prlem936  10938  suplem1pr  10943  axpre-sup  11060  1re  11112  dedekindle  11277  lemul12a  11979  divgt0  11990  divge0  11991  lbreu  12072  sup2  12078  bndndx  12380  elnnz  12478  nzadd  12520  fzind  12571  fnn0ind  12572  uzwo  12809  lbzbi  12834  zmax  12843  zbtwnre  12844  irradd  12871  irrmul  12872  ledivge1le  12963  xrub  13211  supxrunb2  13219  infmremnf  13243  iccid  13290  uzsubsubfz  13446  fzrevral  13512  elfz0fzfz0  13533  fz0fzelfz0  13534  elfzmlbp  13539  elincfzoext  13623  ssfzoulel  13660  ssfzo12bi  13661  fzoopth  13662  elfzonelfzo  13669  elfznelfzo  13673  elfznelfzob  13674  injresinjlem  13690  fleqceilz  13758  modaddmodup  13841  uzindi  13889  suppssfz  13901  mptnn0fsuppr  13906  le2sq2  14042  sqlecan  14116  facdiv  14194  facwordi  14196  faclbnd  14197  hashimarni  14348  hash2prd  14382  hashle2pr  14384  pr2pwpr  14386  fundmge2nop0  14409  fi1uzind  14414  brfi1indALT  14417  swrdnd2  14563  swrdnnn0nd  14564  swrdnd0  14565  pfxnd0  14596  swrdswrdlem  14611  swrdswrd  14612  ccatopth2  14624  wrd2ind  14630  pfxccatin12lem2a  14634  swrdccatin2  14636  pfxccatin12lem2  14638  pfxccatin12lem3  14639  swrdccat  14642  swrdccat3blem  14646  reuccatpfxs1lem  14653  repswswrd  14691  cshwidxmod  14710  cshwidx0  14713  2cshwcshw  14732  cshwcsh2id  14735  cau3lem  15262  caubnd  15266  climrlim2  15454  rlimcn3  15497  mulcn2  15503  climcau  15578  climbdd  15579  caucvg  15586  modfsummod  15701  p1modz1  16170  dvdsle  16221  dvdsdivcl  16227  ltoddhalfle  16272  halfleoddlt  16273  ndvdssub  16320  gcdcllem1  16410  dvdslegcd  16415  bezoutlem4  16453  dfgcd2  16457  lcmf  16544  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem  16552  lcmfdvdsb  16554  lcmfun  16556  coprmdvds1  16563  divgcdcoprm0  16576  cncongr1  16578  cncongr2  16579  prmfac1  16631  pcqcl  16768  dvdsprmpweqle  16798  oddprmdvds  16815  prmpwdvds  16816  infpnlem1  16822  prmgaplem5  16967  prmgaplem6  16968  prmgaplem7  16969  cshwshashlem1  17007  cictr  17712  initoeu2lem1  17921  initoeu2  17923  clatleglb  18424  lidrididd  18578  mulgaddcom  19011  mulginvcom  19012  cycsubm  19115  cyccom  19116  gsmsymgreqlem2  19344  symggen  19383  psgnunilem4  19410  sylow2blem3  19535  frgpnabllem1  19786  imasabl  19789  dprddisj2  19954  lmodfopnelem1  20832  lssssr  20888  lss1d  20897  lspsncv0  21084  rnglidlmcl  21154  rngqiprngimfo  21239  nzerooringczr  21418  pzriprnglem5  21423  pzriprnglem8  21426  znrrg  21503  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  28884  ax5seglem5  28912  axcontlem4  28946  axcontlem10  28952  umgrnloopv  29085  umgrnloop  29087  upgredgpr  29121  numedglnl  29123  usgrausgrb  29148  usgrnloopvALT  29180  usgrnloopALT  29182  usgredg2vlem2  29205  ushgredgedg  29208  ushgredgedgloop  29210  upgrreslem  29283  umgrreslem  29284  nbgr0edglem  29335  nbusgrvtxm1  29358  uvtxnbgrvtx  29372  cusgredg  29403  cusgrres  29428  cusgrsize2inds  29433  cusgrfi  29438  fusgrregdegfi  29549  ewlkle  29585  uspgr2wlkeqi  29627  lfgrwlkprop  29665  lfgrwlknloop  29667  pthdivtx  29706  2pthnloop  29710  upgrwlkdvdelem  29715  upgrspthswlk  29717  usgr2wlkneq  29735  usgr2trlncl  29739  usgr2pthlem  29742  usgr2pth  29743  uspgrn2crct  29787  crctcshwlkn0lem4  29792  crctcshwlkn0lem5  29793  crctcshwlkn0  29800  wlkiswwlks1  29846  wlkiswwlks2  29854  wlkiswwlksupgr2  29856  wwlksnred  29871  wwlksnext  29872  wwlksnextbi  29873  wwlksnextwrd  29876  wwlksnextinj  29878  wwlksnextproplem2  29889  wwlksnextproplem3  29890  wspthsnonn0vne  29896  wspn0  29903  2pthon3v  29922  umgrwwlks2on  29936  elwspths2on  29939  wpthswwlks2on  29940  clwwlk1loop  29966  clwwlkccatlem  29967  umgrclwwlkge2  29969  clwlkclwwlklem2a4  29975  clwlkclwwlklem2a  29976  clwlkclwwlklem3  29979  clwlkclwwlkf1lem3  29984  clwlkclwwlkfo  29987  clwwisshclwwslemlem  29991  erclwwlkeqlen  29997  erclwwlksym  29999  clwwlkf  30025  clwwlknscsh  30040  erclwwlknsym  30048  clwwlknonex2lem2  30086  clwwlknonex2  30087  upgr3v3e3cycl  30158  upgr4cycl4dv4e  30163  eucrctshift  30221  3vfriswmgr  30256  1to2vfriswmgr  30257  1to3vfriswmgr  30258  n4cyclfrgr  30269  4cyclusnfrgr  30270  frgrnbnb  30271  frgrncvvdeqlem8  30284  frgrwopreg  30301  frgr2wwlk1  30307  frgr2wwlkeqm  30309  2clwwlk2clwwlklem  30324  numclwwlk1lem2fo  30336  wlkl0  30345  numclwlk2lem2f  30355  frgrreggt1  30371  frgrreg  30372  frgrregord013  30373  frgrregord13  30374  frgrogt3nreg  30375  eulplig  30463  nmoub3i  30751  ipasslem5  30813  htthlem  30895  ocin  31274  spansneleq  31548  spansnss  31549  elspansn4  31551  h1datomi  31559  nmopub2tALT  31887  nmfnleub2  31904  hstel2  32197  cvnbtwn  32264  spansncv2  32271  dmdmd  32278  dmdbr3  32283  dmdbr4  32284  dmdbr5  32286  mdsl0  32288  mdexchi  32313  cvexchlem  32346  atcv1  32358  atomli  32360  atcvatlem  32363  atcvat2i  32365  chirredi  32372  mdsymlem3  32383  mdsymlem4  32384  sumdmdii  32393  sumdmdlem  32396  cdj1i  32411  ssrelf  32596  f1o3d  32606  fisshasheq  35157  umgr2cycllem  35182  cvxpconn  35284  satfv0  35400  satfsschain  35406  satfrel  35409  satfdm  35411  satfv0fun  35413  sat1el2xp  35421  gonarlem  35436  goalrlem  35438  satffunlem1lem1  35444  satffunlem2lem1  35446  satffunlem2lem2  35448  satffun  35451  mrsubccat  35560  msubvrs  35602  fundmpss  35809  dfon2lem6  35828  dfon2lem8  35830  dfon2lem9  35831  dfon2  35832  wzel  35864  colinearxfr  36115  btwnconn1lem11  36137  lineintmo  36197  in-ax8  36264  ss-ax8  36265  trer  36356  elicc3  36357  finminlem  36358  nn0prpwlem  36362  fnessref  36397  neibastop2  36401  fgmin  36410  tailfb  36417  ordcmp  36487  ee7.2aOLD  36501  bj-cbvalimt  36679  bj-ceqsalt0  36924  bj-ceqsalt1  36925  isbasisrelowllem1  37395  isbasisrelowllem2  37396  relowlpssretop  37404  fvineqsneu  37451  fvineqsneq  37452  wl-mo3t  37616  finixpnum  37651  matunitlindflem1  37662  matunitlindflem2  37663  poimirlem26  37692  poimirlem27  37693  poimirlem29  37695  ftc1anc  37747  fdc  37791  heibor1lem  37855  ghomco  37937  rngoueqz  37986  unichnidl  38077  dmncan1  38122  ax12indn  38988  lshpdisj  39032  lub0N  39234  glb0N  39238  leat2  39339  hlrelat2  39448  cvrexchlem  39464  cvratlem  39466  atcvrj0  39473  cvrat2  39474  snatpsubN  39795  linepsubN  39797  pmaple  39806  pmapsub  39813  elpaddn0  39845  paddasslem5  39869  trlval2  40208  cdlemn11pre  41255  dihord2pre  41270  mapdordlem2  41682  sn-sup2  42530  fsuppind  42629  pell1qrgap  42913  dford3lem1  43065  hbtlem5  43167  onexlimgt  43282  onsucf1olem  43309  omcl2  43372  tfsconcat0b  43385  ntrneiiso  44130  sbiota1  44473  19.41rg  44589  ee223  44673  or2expropbilem1  47069  funressnfv  47080  fcoresf1  47106  2reuimp  47152  f1oresf1o2  47328  zm1nn  47339  nltle2tri  47350  el1fzopredsuc  47362  modlt0b  47400  mod2addne  47401  elsetpreimafvssdm  47423  imasetpreimafvbijlemf1  47441  iccpartlt  47461  iccpartgt  47464  iccelpart  47470  icceuelpart  47473  iccpartnel  47475  fargshiftfo  47479  fargshiftfva  47480  lswn0  47481  ich2exprop  47508  prsprel  47524  sprsymrelfolem2  47530  sprsymrelfo  47534  poprelb  47561  reuopreuprim  47563  goldbachthlem2  47583  odz2prm2pw  47600  fmtnoprmfac1  47602  fmtnofac2lem  47605  prmdvdsfmtnof1lem2  47622  2pwp1prm  47626  sfprmdvdsmersenne  47640  lighneallem3  47644  requad01  47658  requad2  47660  even3prm2  47756  fppr2odd  47768  fpprwpprb  47777  gbegt5  47798  sbgoldbwt  47814  sbgoldbalt  47818  sbgoldbm  47821  bgoldbtbndlem2  47843  bgoldbtbndlem3  47844  bgoldbtbndlem4  47845  bgoldbtbnd  47846  tgblthelfgott  47852  tgoldbach  47854  isubgredg  47903  grimuhgr  47924  grimcnv  47925  grimco  47926  isuspgrim0  47931  isuspgrimlem  47932  uhgrimisgrgriclem  47967  clnbgrgrimlem  47970  grimedg  47972  grtriprop  47978  cycl3grtri  47984  grimgrtri  47986  isubgr3stgrlem6  48008  uspgrlimlem3  48027  uspgrlimlem4  48028  grlimgrtrilem2  48039  grlicsym  48050  clnbgr3stgrgrlim  48056  clnbgr3stgrgrlic  48057  gpgedg2ov  48103  gpgedg2iv  48104  pgnbgreunbgrlem3  48155  pgnbgreunbgrlem6  48161  upgrwlkupwlk  48177  lmod0rng  48266  ztprmneprm  48384  ply1mulgsumlem1  48424  ply1mulgsumlem2  48425  lcoel0  48466  linindslinci  48486  lindslinindimp2lem4  48499  lindslinindsimp2lem5  48500  snlindsntor  48509  ldepspr  48511  lincresunit2  48516  fllog2  48606  dignn0ldlem  48640  dignn0flhalflem1  48653  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658  itcovalt2  48715  resum2sqorgt0  48747  eenglngeehlnmlem2  48776  rrx2linest  48780  itscnhlc0xyqsol  48803  itsclc0  48809  setrec1lem2  49726  aacllem  49839