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  2626  ralrimdvva  3200  ceqsal1t  3498  ceqsalt  3499  spcimgft  3530  vtoclgft  3536  elabgt  3656  sbciegftOLD  3808  reupick  4309  reusv3  5380  sbcop1  5468  propeqop  5487  pwssun  5550  wefrc  5653  ssrel  5766  ssrelOLD  5767  ssrel2  5769  ssrelrel  5780  ssrelrn  5879  tz7.7  6383  ordtr2  6402  onmindif  6451  unizlim  6482  funssres  6585  f1ssf1  6855  fvmptt  7011  fveqdmss  7073  fvcofneq  7088  funsndifnop  7146  funfvima2  7228  isoini  7336  isopolem  7343  weniso  7352  f1ocnv2d  7665  limsssuc  7850  tfindsg  7861  limomss  7871  findsg  7898  funcnvuni  7933  f1oweALT  7976  funelss  8051  bropopvvv  8094  bropfvvvvlem  8095  bropfvvvv  8096  f1o2ndf1  8126  frxp  8130  soseq  8163  suppfnss  8193  wfrlem12OLD  8339  onfununi  8360  tz7.49  8464  omordi  8583  omlimcl  8595  omass  8597  oeordsuc  8611  nnmordi  8648  nnmord  8649  omabs  8668  xpdom2  9086  infensuc  9174  findcard2  9183  findcard2d  9185  findcard3  9295  findcard3OLD  9296  frfi  9298  xpfiOLD  9336  fsuppres  9410  dffi2  9440  elfiun  9447  ordiso2  9534  ordtypelem7  9543  suc11reg  9638  inf3lem2  9648  noinfep  9679  cantnfle  9690  cantnflem1  9708  cantnf  9712  ttrclss  9739  trcl  9747  epfrs  9750  frr3g  9775  r1sdom  9793  updjud  9953  pr2neOLD  10024  dfac8alem  10048  indcardi  10060  alephordi  10093  dfac12lem3  10165  pwsdompw  10222  cofsmo  10288  cfcoflem  10291  coftr  10292  isf32lem2  10373  isf32lem9  10380  axcc3  10457  domtriomlem  10461  axdc3lem2  10470  axdc3lem4  10472  zorn2lem4  10518  zorn2lem6  10520  zorn2lem7  10521  ttukeylem6  10533  uniimadom  10563  konigthlem  10587  fpwwe2lem7  10656  tskord  10799  tskcard  10800  grupr  10816  gruiin  10829  grudomon  10836  grur1a  10838  genpn0  11022  genpcd  11025  distrlem5pr  11046  psslinpr  11050  ltaddpr  11053  ltexprlem3  11057  ltexprlem6  11060  ltapr  11064  prlem936  11066  suplem1pr  11071  axpre-sup  11188  1re  11240  dedekindle  11404  lemul12a  12104  divgt0  12115  divge0  12116  lbreu  12197  sup2  12203  bndndx  12505  elnnz  12603  nzadd  12645  fzind  12696  fnn0ind  12697  uzwo  12932  lbzbi  12957  zmax  12966  zbtwnre  12967  irradd  12994  irrmul  12995  ledivge1le  13085  xrub  13333  supxrunb2  13341  infmremnf  13365  iccid  13412  uzsubsubfz  13568  fzrevral  13634  elfz0fzfz0  13655  fz0fzelfz0  13656  elfzmlbp  13661  elincfzoext  13744  ssfzoulel  13781  ssfzo12bi  13782  fzoopth  13783  elfzonelfzo  13790  elfznelfzo  13793  elfznelfzob  13794  injresinjlem  13808  fleqceilz  13876  modaddmodup  13957  uzindi  14005  suppssfz  14017  mptnn0fsuppr  14022  le2sq2  14158  sqlecan  14232  facdiv  14310  facwordi  14312  faclbnd  14313  hashimarni  14464  hash2prd  14498  hashle2pr  14500  pr2pwpr  14502  fundmge2nop0  14525  fi1uzind  14530  brfi1indALT  14533  swrdnd2  14678  swrdnnn0nd  14679  swrdnd0  14680  pfxnd0  14711  swrdswrdlem  14727  swrdswrd  14728  ccatopth2  14740  wrd2ind  14746  pfxccatin12lem2a  14750  swrdccatin2  14752  pfxccatin12lem2  14754  pfxccatin12lem3  14755  swrdccat  14758  swrdccat3blem  14762  reuccatpfxs1lem  14769  repswswrd  14807  cshwidxmod  14826  cshwidx0  14829  2cshwcshw  14849  cshwcsh2id  14852  cau3lem  15378  caubnd  15382  climrlim2  15568  rlimcn3  15611  mulcn2  15617  climcau  15692  climbdd  15693  caucvg  15700  modfsummod  15815  p1modz1  16284  dvdsle  16334  dvdsdivcl  16340  ltoddhalfle  16385  halfleoddlt  16386  ndvdssub  16433  gcdcllem1  16523  dvdslegcd  16528  bezoutlem4  16566  dfgcd2  16570  lcmf  16657  lcmfunsnlem1  16661  lcmfunsnlem2lem1  16662  lcmfunsnlem  16665  lcmfdvdsb  16667  lcmfun  16669  coprmdvds1  16676  divgcdcoprm0  16689  cncongr1  16691  cncongr2  16692  prmfac1  16744  pcqcl  16881  dvdsprmpweqle  16911  oddprmdvds  16928  prmpwdvds  16929  infpnlem1  16935  prmgaplem5  17080  prmgaplem6  17081  prmgaplem7  17082  cshwshashlem1  17120  cictr  17823  initoeu2lem1  18032  initoeu2  18034  clatleglb  18533  lidrididd  18653  mulgaddcom  19086  mulginvcom  19087  cycsubm  19190  cyccom  19191  gsmsymgreqlem2  19417  symggen  19456  psgnunilem4  19483  sylow2blem3  19608  frgpnabllem1  19859  imasabl  19862  dprddisj2  20027  lmodfopnelem1  20860  lssssr  20916  lss1d  20925  lspsncv0  21112  rnglidlmcl  21182  rngqiprngimfo  21267  nzerooringczr  21446  pzriprnglem5  21451  pzriprnglem8  21454  znrrg  21531  mplcoe5lem  22002  cply1mul  22239  coe1fzgsumdlem  22246  gsummoncoe1  22251  evl1gsumdlem  22299  mamufacex  22339  dmatelnd  22439  scmataddcl  22459  scmatsubcl  22460  scmatmulcl  22461  smatvscl  22467  mavmulsolcl  22494  mdetdiagid  22543  cramerlem3  22632  pmatcoe1fsupp  22644  cpmatacl  22659  cpmatmcllem  22661  mp2pm2mplem4  22752  chpscmat  22785  chfacfisf  22797  chfacfisfcpmat  22798  uniopn  22840  opnnei  23063  neindisj2  23066  restcls  23124  restntr  23125  tgcnp  23196  subbascn  23197  iscnp4  23206  lpcls  23307  cmpsublem  23342  cmpsub  23343  tgcmp  23344  cmpcld  23345  dfconn2  23362  1stcrest  23396  2ndcdisj  23399  1stccnp  23405  comppfsc  23475  kgencn2  23500  txlm  23591  kqreglem1  23684  filin  23797  isfil2  23799  ufilmax  23850  ufileu  23862  filufint  23863  cfinufil  23871  elfm2  23891  rnelfmlem  23895  rnelfm  23896  flimopn  23918  fbflim2  23920  flffbas  23938  fclsnei  23962  flimfnfcls  23971  fclscmp  23973  fcfnei  23978  cnpfcf  23984  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALTlem4  23993  alexsubALT  23994  ptcmplem4  23998  qustgplem  24064  tsmsres  24087  tsmsxp  24098  metss  24452  metcnp3  24484  ovoliunnul  25465  ovolicc2lem3  25477  dyadmax  25556  itg2le  25697  bddiblnc  25800  itgcn  25803  ellimc3  25837  lhop1  25976  dvfsumrlim  25995  fta1g  26132  dvply2g  26249  fta1  26273  aalioulem3  26299  aalioulem4  26300  ulmcaulem  26360  ulmcau  26361  logbgcd1irr  26761  xrlimcnp  26935  cxploglim  26945  jensen  26956  lgsqrmodndvds  27321  gausslemma2dlem1a  27333  gausslemma2dlem2  27335  gausslemma2dlem3  27336  lgsquad2lem2  27353  2lgslem1a1  27357  2sqlem6  27391  2sq2  27401  2sqnn  27407  2sqreultblem  27416  nosepdmlem  27652  nodenselem8  27660  madebdaylemlrcut  27867  addsprop  27940  addsuniflem  27965  negsprop  27998  mulsprop  28090  mulsuniflem  28109  precsex  28177  onsfi  28304  elnnzs  28346  brbtwn2  28889  ax5seglem5  28917  axcontlem4  28951  axcontlem10  28957  umgrnloopv  29090  umgrnloop  29092  upgredgpr  29126  numedglnl  29128  usgrausgrb  29153  usgrnloopvALT  29185  usgrnloopALT  29187  usgredg2vlem2  29210  ushgredgedg  29213  ushgredgedgloop  29215  upgrreslem  29288  umgrreslem  29289  nbgr0edglem  29340  nbusgrvtxm1  29363  uvtxnbgrvtx  29377  cusgredg  29408  cusgrres  29433  cusgrsize2inds  29438  cusgrfi  29443  fusgrregdegfi  29554  ewlkle  29590  uspgr2wlkeqi  29633  lfgrwlkprop  29672  lfgrwlknloop  29674  pthdivtx  29714  2pthnloop  29718  upgrwlkdvdelem  29723  upgrspthswlk  29725  usgr2wlkneq  29743  usgr2trlncl  29747  usgr2pthlem  29750  usgr2pth  29751  uspgrn2crct  29795  crctcshwlkn0lem4  29800  crctcshwlkn0lem5  29801  crctcshwlkn0  29808  wlkiswwlks1  29854  wlkiswwlks2  29862  wlkiswwlksupgr2  29864  wwlksnred  29879  wwlksnext  29880  wwlksnextbi  29881  wwlksnextwrd  29884  wwlksnextinj  29886  wwlksnextproplem2  29897  wwlksnextproplem3  29898  wspthsnonn0vne  29904  wspn0  29911  2pthon3v  29930  umgrwwlks2on  29944  elwspths2on  29947  wpthswwlks2on  29948  clwwlk1loop  29974  clwwlkccatlem  29975  umgrclwwlkge2  29977  clwlkclwwlklem2a4  29983  clwlkclwwlklem2a  29984  clwlkclwwlklem3  29987  clwlkclwwlkf1lem3  29992  clwlkclwwlkfo  29995  clwwisshclwwslemlem  29999  erclwwlkeqlen  30005  erclwwlksym  30007  clwwlkf  30033  clwwlknscsh  30048  erclwwlknsym  30056  clwwlknonex2lem2  30094  clwwlknonex2  30095  upgr3v3e3cycl  30166  upgr4cycl4dv4e  30171  eucrctshift  30229  3vfriswmgr  30264  1to2vfriswmgr  30265  1to3vfriswmgr  30266  n4cyclfrgr  30277  4cyclusnfrgr  30278  frgrnbnb  30279  frgrncvvdeqlem8  30292  frgrwopreg  30309  frgr2wwlk1  30315  frgr2wwlkeqm  30317  2clwwlk2clwwlklem  30332  numclwwlk1lem2fo  30344  wlkl0  30353  numclwlk2lem2f  30363  frgrreggt1  30379  frgrreg  30380  frgrregord013  30381  frgrregord13  30382  frgrogt3nreg  30383  eulplig  30471  nmoub3i  30759  ipasslem5  30821  htthlem  30903  ocin  31282  spansneleq  31556  spansnss  31557  elspansn4  31559  h1datomi  31567  nmopub2tALT  31895  nmfnleub2  31912  hstel2  32205  cvnbtwn  32272  spansncv2  32279  dmdmd  32286  dmdbr3  32291  dmdbr4  32292  dmdbr5  32294  mdsl0  32296  mdexchi  32321  cvexchlem  32354  atcv1  32366  atomli  32368  atcvatlem  32371  atcvat2i  32373  chirredi  32380  mdsymlem3  32391  mdsymlem4  32392  sumdmdii  32401  sumdmdlem  32404  cdj1i  32419  ssrelf  32600  f1o3d  32610  fisshasheq  35142  umgr2cycllem  35167  cvxpconn  35269  satfv0  35385  satfsschain  35391  satfrel  35394  satfdm  35396  satfv0fun  35398  sat1el2xp  35406  gonarlem  35421  goalrlem  35423  satffunlem1lem1  35429  satffunlem2lem1  35431  satffunlem2lem2  35433  satffun  35436  mrsubccat  35545  msubvrs  35587  fundmpss  35789  dfon2lem6  35811  dfon2lem8  35813  dfon2lem9  35814  dfon2  35815  wzel  35847  colinearxfr  36098  btwnconn1lem11  36120  lineintmo  36180  in-ax8  36247  ss-ax8  36248  trer  36339  elicc3  36340  finminlem  36341  nn0prpwlem  36345  fnessref  36380  neibastop2  36384  fgmin  36393  tailfb  36400  ordcmp  36470  ee7.2aOLD  36484  bj-cbvalimt  36662  bj-ceqsalt0  36907  bj-ceqsalt1  36908  isbasisrelowllem1  37378  isbasisrelowllem2  37379  relowlpssretop  37387  fvineqsneu  37434  fvineqsneq  37435  wl-mo3t  37599  finixpnum  37634  matunitlindflem1  37645  matunitlindflem2  37646  poimirlem26  37675  poimirlem27  37676  poimirlem29  37678  ftc1anc  37730  fdc  37774  heibor1lem  37838  ghomco  37920  rngoueqz  37969  unichnidl  38060  dmncan1  38105  ax12indn  38966  lshpdisj  39010  lub0N  39212  glb0N  39216  leat2  39317  hlrelat2  39427  cvrexchlem  39443  cvratlem  39445  atcvrj0  39452  cvrat2  39453  snatpsubN  39774  linepsubN  39776  pmaple  39785  pmapsub  39792  elpaddn0  39824  paddasslem5  39848  trlval2  40187  cdlemn11pre  41234  dihord2pre  41249  mapdordlem2  41661  sn-sup2  42489  fsuppind  42588  pell1qrgap  42872  dford3lem1  43025  hbtlem5  43127  onexlimgt  43242  onsucf1olem  43269  omcl2  43332  tfsconcat0b  43345  ntrneiiso  44090  sbiota1  44433  19.41rg  44550  ee223  44634  or2expropbilem1  47041  funressnfv  47052  fcoresf1  47078  2reuimp  47124  f1oresf1o2  47300  zm1nn  47311  nltle2tri  47322  el1fzopredsuc  47334  elsetpreimafvssdm  47380  imasetpreimafvbijlemf1  47398  iccpartlt  47418  iccpartgt  47421  iccelpart  47427  icceuelpart  47430  iccpartnel  47432  fargshiftfo  47436  fargshiftfva  47437  lswn0  47438  ich2exprop  47465  prsprel  47481  sprsymrelfolem2  47487  sprsymrelfo  47491  poprelb  47518  reuopreuprim  47520  goldbachthlem2  47540  odz2prm2pw  47557  fmtnoprmfac1  47559  fmtnofac2lem  47562  prmdvdsfmtnof1lem2  47579  2pwp1prm  47583  sfprmdvdsmersenne  47597  lighneallem3  47601  requad01  47615  requad2  47617  even3prm2  47713  fppr2odd  47725  fpprwpprb  47734  gbegt5  47755  sbgoldbwt  47771  sbgoldbalt  47775  sbgoldbm  47778  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  tgblthelfgott  47809  tgoldbach  47811  isubgredg  47859  grimuhgr  47880  grimcnv  47881  grimco  47882  isuspgrim0  47887  isuspgrimlem  47888  uhgrimisgrgriclem  47923  clnbgrgrimlem  47926  grimedg  47928  grtriprop  47933  cycl3grtri  47939  grimgrtri  47941  isubgr3stgrlem6  47963  uspgrlimlem3  47982  uspgrlimlem4  47983  grlimgrtrilem2  47987  grlicsym  47998  clnbgr3stgrgrlic  48004  upgrwlkupwlk  48095  lmod0rng  48184  ztprmneprm  48302  ply1mulgsumlem1  48342  ply1mulgsumlem2  48343  lcoel0  48384  linindslinci  48404  lindslinindimp2lem4  48417  lindslinindsimp2lem5  48418  snlindsntor  48427  ldepspr  48429  lincresunit2  48434  fllog2  48528  dignn0ldlem  48562  dignn0flhalflem1  48575  nn0sumshdiglemA  48579  nn0sumshdiglemB  48580  itcovalt2  48637  resum2sqorgt0  48669  eenglngeehlnmlem2  48698  rrx2linest  48702  itscnhlc0xyqsol  48725  itsclc0  48731  setrec1lem2  49532  aacllem  49645