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  2245  moexexlem  2623  ralrimdvva  3208  ceqsal1t  3511  ceqsalt  3512  spcimgft  3545  vtoclgft  3551  elabgt  3671  sbciegftOLD  3829  reupick  4334  reusv3  5410  sbcop1  5498  propeqop  5516  pwssun  5579  wefrc  5682  ssrel  5794  ssrelOLD  5795  ssrel2  5797  ssrelrel  5808  ssrelrn  5907  tz7.7  6411  ordtr2  6429  onmindif  6477  unizlim  6508  funssres  6611  f1ssf1  6880  fvmptt  7035  fveqdmss  7097  fvcofneq  7112  funsndifnop  7170  funfvima2  7250  isoini  7357  isopolem  7364  weniso  7373  f1ocnv2d  7685  limsssuc  7870  tfindsg  7881  limomss  7891  findsg  7919  funcnvuni  7954  f1oweALT  7995  funelss  8070  bropopvvv  8113  bropfvvvvlem  8114  bropfvvvv  8115  f1o2ndf1  8145  frxp  8149  soseq  8182  suppfnss  8212  wfrlem12OLD  8358  onfununi  8379  tz7.49  8483  omordi  8602  omlimcl  8614  omass  8616  oeordsuc  8630  nnmordi  8667  nnmord  8668  omabs  8687  xpdom2  9105  infensuc  9193  findcard2  9202  findcard2d  9204  findcard3  9315  findcard3OLD  9316  frfi  9318  xpfiOLD  9356  fsuppres  9430  dffi2  9460  elfiun  9467  ordiso2  9552  ordtypelem7  9561  suc11reg  9656  inf3lem2  9666  noinfep  9697  cantnfle  9708  cantnflem1  9726  cantnf  9730  ttrclss  9757  trcl  9765  epfrs  9768  frr3g  9793  r1sdom  9811  updjud  9971  pr2neOLD  10042  dfac8alem  10066  indcardi  10078  alephordi  10111  dfac12lem3  10183  pwsdompw  10240  cofsmo  10306  cfcoflem  10309  coftr  10310  isf32lem2  10391  isf32lem9  10398  axcc3  10475  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  zorn2lem4  10536  zorn2lem6  10538  zorn2lem7  10539  ttukeylem6  10551  uniimadom  10581  konigthlem  10605  fpwwe2lem7  10674  tskord  10817  tskcard  10818  grupr  10834  gruiin  10847  grudomon  10854  grur1a  10856  genpn0  11040  genpcd  11043  distrlem5pr  11064  psslinpr  11068  ltaddpr  11071  ltexprlem3  11075  ltexprlem6  11078  ltapr  11082  prlem936  11084  suplem1pr  11089  axpre-sup  11206  1re  11258  dedekindle  11422  lemul12a  12122  divgt0  12133  divge0  12134  lbreu  12215  sup2  12221  bndndx  12522  elnnz  12620  nzadd  12662  fzind  12713  fnn0ind  12714  uzwo  12950  lbzbi  12975  zmax  12984  zbtwnre  12985  irradd  13012  irrmul  13013  ledivge1le  13103  xrub  13350  supxrunb2  13358  infmremnf  13381  iccid  13428  uzsubsubfz  13582  fzrevral  13648  elfz0fzfz0  13669  fz0fzelfz0  13670  elfzmlbp  13675  elincfzoext  13758  ssfzoulel  13795  ssfzo12bi  13796  fzoopth  13797  elfzonelfzo  13804  elfznelfzo  13807  elfznelfzob  13808  injresinjlem  13822  fleqceilz  13890  modaddmodup  13971  uzindi  14019  suppssfz  14031  mptnn0fsuppr  14036  le2sq2  14171  sqlecan  14244  facdiv  14322  facwordi  14324  faclbnd  14325  hashimarni  14476  hash2prd  14510  hashle2pr  14512  pr2pwpr  14514  fundmge2nop0  14537  fi1uzind  14542  brfi1indALT  14545  swrdnd2  14689  swrdnnn0nd  14690  swrdnd0  14691  pfxnd0  14722  swrdswrdlem  14738  swrdswrd  14739  ccatopth2  14751  wrd2ind  14757  pfxccatin12lem2a  14761  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12lem3  14766  swrdccat  14769  swrdccat3blem  14773  reuccatpfxs1lem  14780  repswswrd  14818  cshwidxmod  14837  cshwidx0  14840  2cshwcshw  14860  cshwcsh2id  14863  cau3lem  15389  caubnd  15393  climrlim2  15579  rlimcn3  15622  mulcn2  15628  climcau  15703  climbdd  15704  caucvg  15711  modfsummod  15826  p1modz1  16293  dvdsle  16343  dvdsdivcl  16349  ltoddhalfle  16394  halfleoddlt  16395  ndvdssub  16442  gcdcllem1  16532  dvdslegcd  16537  bezoutlem4  16575  dfgcd2  16579  lcmf  16666  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem  16674  lcmfdvdsb  16676  lcmfun  16678  coprmdvds1  16685  divgcdcoprm0  16698  cncongr1  16700  cncongr2  16701  prmfac1  16753  pcqcl  16889  dvdsprmpweqle  16919  oddprmdvds  16936  prmpwdvds  16937  infpnlem1  16943  prmgaplem5  17088  prmgaplem6  17089  prmgaplem7  17090  cshwshashlem1  17129  cictr  17852  initoeu2lem1  18067  initoeu2  18069  clatleglb  18575  lidrididd  18695  mulgaddcom  19128  mulginvcom  19129  cycsubm  19232  cyccom  19233  gsmsymgreqlem2  19463  symggen  19502  psgnunilem4  19529  sylow2blem3  19654  frgpnabllem1  19905  imasabl  19908  dprddisj2  20073  lmodfopnelem1  20912  lssssr  20969  lss1d  20978  lspsncv0  21165  rnglidlmcl  21243  rngqiprngimfo  21328  nzerooringczr  21508  pzriprnglem5  21513  pzriprnglem8  21516  znrrg  21601  mplcoe5lem  22074  cply1mul  22315  coe1fzgsumdlem  22322  gsummoncoe1  22327  evl1gsumdlem  22375  mamufacex  22415  dmatelnd  22517  scmataddcl  22537  scmatsubcl  22538  scmatmulcl  22539  smatvscl  22545  mavmulsolcl  22572  mdetdiagid  22621  cramerlem3  22710  pmatcoe1fsupp  22722  cpmatacl  22737  cpmatmcllem  22739  mp2pm2mplem4  22830  chpscmat  22863  chfacfisf  22875  chfacfisfcpmat  22876  uniopn  22918  opnnei  23143  neindisj2  23146  restcls  23204  restntr  23205  tgcnp  23276  subbascn  23277  iscnp4  23286  lpcls  23387  cmpsublem  23422  cmpsub  23423  tgcmp  23424  cmpcld  23425  dfconn2  23442  1stcrest  23476  2ndcdisj  23479  1stccnp  23485  comppfsc  23555  kgencn2  23580  txlm  23671  kqreglem1  23764  filin  23877  isfil2  23879  ufilmax  23930  ufileu  23942  filufint  23943  cfinufil  23951  elfm2  23971  rnelfmlem  23975  rnelfm  23976  flimopn  23998  fbflim2  24000  flffbas  24018  fclsnei  24042  flimfnfcls  24051  fclscmp  24053  fcfnei  24058  cnpfcf  24064  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  ptcmplem4  24078  qustgplem  24144  tsmsres  24167  tsmsxp  24178  metss  24536  metcnp3  24568  ovoliunnul  25555  ovolicc2lem3  25567  dyadmax  25646  itg2le  25788  bddiblnc  25891  itgcn  25894  ellimc3  25928  lhop1  26067  dvfsumrlim  26086  fta1g  26223  dvply2g  26340  fta1  26364  aalioulem3  26390  aalioulem4  26391  ulmcaulem  26451  ulmcau  26452  logbgcd1irr  26851  xrlimcnp  27025  cxploglim  27035  jensen  27046  lgsqrmodndvds  27411  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem3  27426  lgsquad2lem2  27443  2lgslem1a1  27447  2sqlem6  27481  2sq2  27491  2sqnn  27497  2sqreultblem  27506  nosepdmlem  27742  nodenselem8  27750  madebdaylemlrcut  27951  addsprop  28023  addsuniflem  28048  negsprop  28081  mulsprop  28170  mulsuniflem  28189  precsex  28256  elnnzs  28401  brbtwn2  28934  ax5seglem5  28962  axcontlem4  28996  axcontlem10  29002  umgrnloopv  29137  umgrnloop  29139  upgredgpr  29173  numedglnl  29175  usgrausgrb  29200  usgrnloopvALT  29232  usgrnloopALT  29234  usgredg2vlem2  29257  ushgredgedg  29260  ushgredgedgloop  29262  upgrreslem  29335  umgrreslem  29336  nbgr0edglem  29387  nbusgrvtxm1  29410  uvtxnbgrvtx  29424  cusgredg  29455  cusgrres  29480  cusgrsize2inds  29485  cusgrfi  29490  fusgrregdegfi  29601  ewlkle  29637  uspgr2wlkeqi  29680  lfgrwlkprop  29719  lfgrwlknloop  29721  pthdivtx  29761  2pthnloop  29763  upgrwlkdvdelem  29768  upgrspthswlk  29770  usgr2wlkneq  29788  usgr2trlncl  29792  usgr2pthlem  29795  usgr2pth  29796  uspgrn2crct  29837  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0  29850  wlkiswwlks1  29896  wlkiswwlks2  29904  wlkiswwlksupgr2  29906  wwlksnred  29921  wwlksnext  29922  wwlksnextbi  29923  wwlksnextwrd  29926  wwlksnextinj  29928  wwlksnextproplem2  29939  wwlksnextproplem3  29940  wspthsnonn0vne  29946  wspn0  29953  2pthon3v  29972  umgrwwlks2on  29986  elwspths2on  29989  wpthswwlks2on  29990  clwwlk1loop  30016  clwwlkccatlem  30017  umgrclwwlkge2  30019  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem3  30029  clwlkclwwlkf1lem3  30034  clwlkclwwlkfo  30037  clwwisshclwwslemlem  30041  erclwwlkeqlen  30047  erclwwlksym  30049  clwwlkf  30075  clwwlknscsh  30090  erclwwlknsym  30098  clwwlknonex2lem2  30136  clwwlknonex2  30137  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eucrctshift  30271  3vfriswmgr  30306  1to2vfriswmgr  30307  1to3vfriswmgr  30308  n4cyclfrgr  30319  4cyclusnfrgr  30320  frgrnbnb  30321  frgrncvvdeqlem8  30334  frgrwopreg  30351  frgr2wwlk1  30357  frgr2wwlkeqm  30359  2clwwlk2clwwlklem  30374  numclwwlk1lem2fo  30386  wlkl0  30395  numclwlk2lem2f  30405  frgrreggt1  30421  frgrreg  30422  frgrregord013  30423  frgrregord13  30424  frgrogt3nreg  30425  eulplig  30513  nmoub3i  30801  ipasslem5  30863  htthlem  30945  ocin  31324  spansneleq  31598  spansnss  31599  elspansn4  31601  h1datomi  31609  nmopub2tALT  31937  nmfnleub2  31954  hstel2  32247  cvnbtwn  32314  spansncv2  32321  dmdmd  32328  dmdbr3  32333  dmdbr4  32334  dmdbr5  32336  mdsl0  32338  mdexchi  32363  cvexchlem  32396  atcv1  32408  atomli  32410  atcvatlem  32413  atcvat2i  32415  chirredi  32422  mdsymlem3  32433  mdsymlem4  32434  sumdmdii  32443  sumdmdlem  32446  cdj1i  32461  ssrelf  32634  f1o3d  32643  fisshasheq  35098  umgr2cycllem  35124  cvxpconn  35226  satfv0  35342  satfsschain  35348  satfrel  35351  satfdm  35353  satfv0fun  35355  sat1el2xp  35363  gonarlem  35378  goalrlem  35380  satffunlem1lem1  35386  satffunlem2lem1  35388  satffunlem2lem2  35390  satffun  35393  mrsubccat  35502  msubvrs  35544  fundmpss  35747  dfon2lem6  35769  dfon2lem8  35771  dfon2lem9  35772  dfon2  35773  wzel  35805  colinearxfr  36056  btwnconn1lem11  36078  lineintmo  36138  in-ax8  36206  ss-ax8  36207  trer  36298  elicc3  36299  finminlem  36300  nn0prpwlem  36304  fnessref  36339  neibastop2  36343  fgmin  36352  tailfb  36359  ordcmp  36429  ee7.2aOLD  36443  bj-cbvalimt  36621  bj-ceqsalt0  36866  bj-ceqsalt1  36867  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlpssretop  37346  fvineqsneu  37393  fvineqsneq  37394  wl-mo3t  37556  finixpnum  37591  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  ftc1anc  37687  fdc  37731  heibor1lem  37795  ghomco  37877  rngoueqz  37926  unichnidl  38017  dmncan1  38062  ax12indn  38924  lshpdisj  38968  lub0N  39170  glb0N  39174  leat2  39275  hlrelat2  39385  cvrexchlem  39401  cvratlem  39403  atcvrj0  39410  cvrat2  39411  snatpsubN  39732  linepsubN  39734  pmaple  39743  pmapsub  39750  elpaddn0  39782  paddasslem5  39806  trlval2  40145  cdlemn11pre  41192  dihord2pre  41207  mapdordlem2  41619  sn-sup2  42477  fsuppind  42576  pell1qrgap  42861  dford3lem1  43014  hbtlem5  43116  onexlimgt  43231  onsucf1olem  43259  omcl2  43322  tfsconcat0b  43335  ntrneiiso  44080  sbiota1  44429  19.41rg  44547  ee223  44631  or2expropbilem1  46981  funressnfv  46992  fcoresf1  47018  2reuimp  47064  f1oresf1o2  47240  zm1nn  47251  nltle2tri  47262  el1fzopredsuc  47274  elsetpreimafvssdm  47310  imasetpreimafvbijlemf1  47328  iccpartlt  47348  iccpartgt  47351  iccelpart  47357  icceuelpart  47360  iccpartnel  47362  fargshiftfo  47366  fargshiftfva  47367  lswn0  47368  ich2exprop  47395  prsprel  47411  sprsymrelfolem2  47417  sprsymrelfo  47421  poprelb  47448  reuopreuprim  47450  goldbachthlem2  47470  odz2prm2pw  47487  fmtnoprmfac1  47489  fmtnofac2lem  47492  prmdvdsfmtnof1lem2  47509  2pwp1prm  47513  sfprmdvdsmersenne  47527  lighneallem3  47531  requad01  47545  requad2  47547  even3prm2  47643  fppr2odd  47655  fpprwpprb  47664  gbegt5  47685  sbgoldbwt  47701  sbgoldbalt  47705  sbgoldbm  47708  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  tgblthelfgott  47739  tgoldbach  47741  isubgredg  47789  isuspgrim0  47809  isuspgrimlem  47811  grimuhgr  47815  grimcnv  47816  grimco  47817  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838  grimedg  47840  grtriprop  47845  grimgrtri  47851  isubgr3stgrlem6  47873  uspgrlimlem3  47892  uspgrlimlem4  47893  grlimgrtrilem2  47897  grlicsym  47908  clnbgr3stgrgrlic  47914  upgrwlkupwlk  47983  lmod0rng  48072  ztprmneprm  48191  ply1mulgsumlem1  48231  ply1mulgsumlem2  48232  lcoel0  48273  linindslinci  48293  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  snlindsntor  48316  ldepspr  48318  lincresunit2  48323  fllog2  48417  dignn0ldlem  48451  dignn0flhalflem1  48464  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  itcovalt2  48526  resum2sqorgt0  48558  eenglngeehlnmlem2  48587  rrx2linest  48591  itscnhlc0xyqsol  48614  itsclc0  48620  setrec1lem2  48918  aacllem  49031