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  412  expcomd  417  impancom  452  a2and  842  dedlem0b  1042  sbequ1  2241  moexexlem  2629  ralrimdvva  3126  ceqsalt  3463  vtoclgft  3493  sbciegft  3755  reupick  4253  reusv3  5329  sbcop1  5403  propeqop  5422  pwssun  5486  wefrc  5584  ssrel  5694  ssrelOLD  5695  ssrel2  5697  ssrelrel  5708  ssrelrn  5806  tz7.7  6296  ordtr2  6314  onmindif  6359  unizlim  6387  funssres  6485  f1ssf1  6757  fvmptt  6904  fveqdmss  6965  fvcofneq  6978  funsndifnop  7032  funfvima2  7116  isoini  7218  isopolem  7225  weniso  7234  f1ocnv2d  7531  limsssuc  7706  tfindsg  7716  limomss  7726  findsg  7755  funcnvuni  7787  f1oweALT  7824  funelss  7897  bropopvvv  7939  bropfvvvvlem  7940  bropfvvvv  7941  f1o2ndf1  7972  frxp  7976  suppfnss  8014  wfrlem12OLD  8160  onfununi  8181  tz7.49  8285  omordi  8406  omlimcl  8418  omass  8420  oeordsuc  8434  nnmordi  8471  nnmord  8472  omabs  8490  xpdom2  8863  infensuc  8951  findcard2  8956  findcard2d  8958  findcard2OLD  9065  findcard3  9066  frfi  9068  xpfi  9094  fsuppres  9162  dffi2  9191  elfiun  9198  ordiso2  9283  ordtypelem7  9292  suc11reg  9386  inf3lem2  9396  noinfep  9427  cantnfle  9438  cantnflem1  9456  cantnf  9460  ttrclss  9487  trcl  9495  epfrs  9498  frr3g  9523  r1sdom  9541  updjud  9701  pr2ne  9770  dfac8alem  9794  indcardi  9806  alephordi  9839  dfac12lem3  9910  pwsdompw  9969  cofsmo  10034  cfcoflem  10037  coftr  10038  isf32lem2  10119  isf32lem9  10126  axcc3  10203  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  zorn2lem4  10264  zorn2lem6  10266  zorn2lem7  10267  ttukeylem6  10279  uniimadom  10309  konigthlem  10333  fpwwe2lem7  10402  tskord  10545  tskcard  10546  grupr  10562  gruiin  10575  grudomon  10582  grur1a  10584  genpn0  10768  genpcd  10771  distrlem5pr  10792  psslinpr  10796  ltaddpr  10799  ltexprlem3  10803  ltexprlem6  10806  ltapr  10810  prlem936  10812  suplem1pr  10817  axpre-sup  10934  1re  10984  dedekindle  11148  lemul12a  11842  divgt0  11852  divge0  11853  lbreu  11934  sup2  11940  bndndx  12241  elnnz  12338  nzadd  12377  fzind  12427  fnn0ind  12428  uzwo  12660  lbzbi  12685  zmax  12694  zbtwnre  12695  irradd  12722  irrmul  12723  ledivge1le  12810  xrub  13055  supxrunb2  13063  infmremnf  13086  iccid  13133  uzsubsubfz  13287  fzrevral  13350  elfz0fzfz0  13370  fz0fzelfz0  13371  elfzmlbp  13376  elincfzoext  13454  ssfzoulel  13490  ssfzo12bi  13491  elfzonelfzo  13498  elfznelfzo  13501  elfznelfzob  13502  injresinjlem  13516  fleqceilz  13583  modaddmodup  13663  uzindi  13711  suppssfz  13723  mptnn0fsuppr  13728  le2sq2  13863  sqlecan  13934  facdiv  14010  facwordi  14012  faclbnd  14013  hashimarni  14165  hash2prd  14198  hashle2pr  14200  pr2pwpr  14202  fundmge2nop0  14215  fi1uzind  14220  brfi1indALT  14223  swrdnd2  14377  swrdnnn0nd  14378  swrdnd0  14379  pfxnd0  14410  swrdswrdlem  14426  swrdswrd  14427  ccatopth2  14439  wrd2ind  14445  pfxccatin12lem2a  14449  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12lem3  14454  swrdccat  14457  swrdccat3blem  14461  reuccatpfxs1lem  14468  repswswrd  14506  cshwidxmod  14525  cshwidx0  14528  2cshwcshw  14547  cshwcsh2id  14550  cau3lem  15075  caubnd  15079  climrlim2  15265  rlimcn3  15308  mulcn2  15314  climcau  15391  climbdd  15392  caucvg  15399  modfsummod  15515  p1modz1  15979  dvdsle  16028  dvdsdivcl  16034  ltoddhalfle  16079  halfleoddlt  16080  ndvdssub  16127  gcdcllem1  16215  dvdslegcd  16220  bezoutlem4  16259  dfgcd2  16263  lcmf  16347  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem  16355  lcmfdvdsb  16357  lcmfun  16359  coprmdvds1  16366  divgcdcoprm0  16379  cncongr1  16381  cncongr2  16382  prmfac1  16435  pcqcl  16566  dvdsprmpweqle  16596  oddprmdvds  16613  prmpwdvds  16614  infpnlem1  16620  prmgaplem5  16765  prmgaplem6  16766  prmgaplem7  16767  cshwshashlem1  16806  cictr  17526  initoeu2lem1  17738  initoeu2  17740  clatleglb  18245  lidrididd  18363  mulgaddcom  18736  mulginvcom  18737  cycsubm  18830  cyccom  18831  gsmsymgreqlem2  19048  symggen  19087  psgnunilem4  19114  sylow2blem3  19236  frgpnabllem1  19483  dprddisj2  19651  f1rhm0to0ALT  19994  lmodfopnelem1  20168  lssssr  20224  lss1d  20234  lspsncv0  20417  znrrg  20782  mplcoe5lem  21249  cply1mul  21474  coe1fzgsumdlem  21481  gsummoncoe1  21484  evl1gsumdlem  21531  mamufacex  21547  dmatelnd  21654  scmataddcl  21674  scmatsubcl  21675  scmatmulcl  21676  smatvscl  21682  mavmulsolcl  21709  mdetdiagid  21758  cramerlem3  21847  pmatcoe1fsupp  21859  cpmatacl  21874  cpmatmcllem  21876  mp2pm2mplem4  21967  chpscmat  22000  chfacfisf  22012  chfacfisfcpmat  22013  uniopn  22055  opnnei  22280  neindisj2  22283  restcls  22341  restntr  22342  tgcnp  22413  subbascn  22414  iscnp4  22423  lpcls  22524  cmpsublem  22559  cmpsub  22560  tgcmp  22561  cmpcld  22562  dfconn2  22579  1stcrest  22613  2ndcdisj  22616  1stccnp  22622  comppfsc  22692  kgencn2  22717  txlm  22808  kqreglem1  22901  filin  23014  isfil2  23016  ufilmax  23067  ufileu  23079  filufint  23080  cfinufil  23088  elfm2  23108  rnelfmlem  23112  rnelfm  23113  flimopn  23135  fbflim2  23137  flffbas  23155  fclsnei  23179  flimfnfcls  23188  fclscmp  23190  fcfnei  23195  cnpfcf  23201  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  alexsubALT  23211  ptcmplem4  23215  qustgplem  23281  tsmsres  23304  tsmsxp  23315  metss  23673  metcnp3  23705  ovoliunnul  24680  ovolicc2lem3  24692  dyadmax  24771  itg2le  24913  bddiblnc  25015  itgcn  25018  ellimc3  25052  lhop1  25187  dvfsumrlim  25204  fta1g  25341  fta1  25477  aalioulem3  25503  aalioulem4  25504  ulmcaulem  25562  ulmcau  25563  logbgcd1irr  25953  xrlimcnp  26127  cxploglim  26136  jensen  26147  lgsqrmodndvds  26510  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  gausslemma2dlem3  26525  lgsquad2lem2  26542  2lgslem1a1  26546  2sqlem6  26580  2sq2  26590  2sqnn  26596  2sqreultblem  26605  brbtwn2  27282  ax5seglem5  27310  axcontlem4  27344  axcontlem10  27350  umgrnloopv  27485  umgrnloop  27487  upgredgpr  27521  numedglnl  27523  usgrausgrb  27548  usgrnloopvALT  27577  usgrnloopALT  27579  usgredg2vlem2  27602  ushgredgedg  27605  ushgredgedgloop  27607  upgrreslem  27680  umgrreslem  27681  nbgr0vtxlem  27731  nbusgrvtxm1  27755  uvtxnbgrvtx  27769  cusgredg  27800  cusgrres  27824  cusgrsize2inds  27829  cusgrfi  27834  fusgrregdegfi  27945  ewlkle  27981  uspgr2wlkeqi  28024  wlklenvclwlkOLD  28032  lfgrwlkprop  28064  lfgrwlknloop  28066  pthdivtx  28106  2pthnloop  28108  upgrwlkdvdelem  28113  upgrspthswlk  28115  usgr2wlkneq  28133  usgr2trlncl  28137  usgr2pthlem  28140  usgr2pth  28141  uspgrn2crct  28182  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0  28195  wlkiswwlks1  28241  wlkiswwlks2  28249  wlkiswwlksupgr2  28251  wwlksnred  28266  wwlksnext  28267  wwlksnextbi  28268  wwlksnextwrd  28271  wwlksnextinj  28273  wwlksnextproplem2  28284  wwlksnextproplem3  28285  wspthsnonn0vne  28291  wspn0  28298  2pthon3v  28317  umgrwwlks2on  28331  elwspths2on  28334  wpthswwlks2on  28335  clwwlk1loop  28361  clwwlkccatlem  28362  umgrclwwlkge2  28364  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlklem3  28374  clwlkclwwlkf1lem3  28379  clwlkclwwlkfo  28382  clwwisshclwwslemlem  28386  erclwwlkeqlen  28392  erclwwlksym  28394  clwwlkf  28420  clwwlknscsh  28435  erclwwlknsym  28443  clwwlknonex2lem2  28481  clwwlknonex2  28482  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  eucrctshift  28616  3vfriswmgr  28651  1to2vfriswmgr  28652  1to3vfriswmgr  28653  n4cyclfrgr  28664  4cyclusnfrgr  28665  frgrnbnb  28666  frgrncvvdeqlem8  28679  frgrwopreg  28696  frgr2wwlk1  28702  frgr2wwlkeqm  28704  2clwwlk2clwwlklem  28719  numclwwlk1lem2fo  28731  wlkl0  28740  numclwlk2lem2f  28750  frgrreggt1  28766  frgrreg  28767  frgrregord013  28768  frgrregord13  28769  frgrogt3nreg  28770  eulplig  28856  nmoub3i  29144  ipasslem5  29206  htthlem  29288  ocin  29667  spansneleq  29941  spansnss  29942  elspansn4  29944  h1datomi  29952  nmopub2tALT  30280  nmfnleub2  30297  hstel2  30590  cvnbtwn  30657  spansncv2  30664  dmdmd  30671  dmdbr3  30676  dmdbr4  30677  dmdbr5  30679  mdsl0  30681  mdexchi  30706  cvexchlem  30739  atcv1  30751  atomli  30753  atcvatlem  30756  atcvat2i  30758  chirredi  30765  mdsymlem3  30776  mdsymlem4  30777  sumdmdii  30786  sumdmdlem  30789  cdj1i  30804  ssrelf  30964  f1o3d  30971  fisshasheq  33082  umgr2cycllem  33111  cvxpconn  33213  satfv0  33329  satfsschain  33335  satfrel  33338  satfdm  33340  satfv0fun  33342  sat1el2xp  33350  gonarlem  33365  goalrlem  33367  satffunlem1lem1  33373  satffunlem2lem1  33375  satffunlem2lem2  33377  satffun  33380  mrsubccat  33489  msubvrs  33531  fundmpss  33749  dfon2lem6  33773  dfon2lem8  33775  dfon2lem9  33776  dfon2  33777  soseq  33812  wzel  33827  nosepdmlem  33895  nodenselem8  33903  madebdaylemlrcut  34088  colinearxfr  34386  btwnconn1lem11  34408  lineintmo  34468  trer  34514  elicc3  34515  finminlem  34516  nn0prpwlem  34520  fnessref  34555  neibastop2  34559  fgmin  34568  tailfb  34575  ordcmp  34645  ee7.2aOLD  34659  bj-cbvalimt  34829  bj-ceqsalt0  35078  bj-ceqsalt1  35079  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlpssretop  35544  fvineqsneu  35591  fvineqsneq  35592  wl-mo3t  35740  finixpnum  35771  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  ftc1anc  35867  fdc  35912  heibor1lem  35976  ghomco  36058  rngoueqz  36107  unichnidl  36198  dmncan1  36243  ax12indn  36964  lshpdisj  37008  lub0N  37210  glb0N  37214  leat2  37315  hlrelat2  37424  cvrexchlem  37440  cvratlem  37442  atcvrj0  37449  cvrat2  37450  snatpsubN  37771  linepsubN  37773  pmaple  37782  pmapsub  37789  elpaddn0  37821  paddasslem5  37845  trlval2  38184  cdlemn11pre  39231  dihord2pre  39246  mapdordlem2  39658  fsuppind  40286  sn-sup2  40446  pell1qrgap  40703  dford3lem1  40855  hbtlem5  40960  ntrneiiso  41708  sbiota1  42059  19.41rg  42177  ee223  42261  or2expropbilem1  44537  funressnfv  44548  fcoresf1  44574  2reuimp  44618  f1oresf1o2  44794  zm1nn  44805  nltle2tri  44816  el1fzopredsuc  44828  fzoopth  44830  elsetpreimafvssdm  44849  imasetpreimafvbijlemf1  44867  iccpartlt  44887  iccpartgt  44890  iccelpart  44896  icceuelpart  44899  iccpartnel  44901  fargshiftfo  44905  fargshiftfva  44906  lswn0  44907  ich2exprop  44934  prsprel  44950  sprsymrelfolem2  44956  sprsymrelfo  44960  poprelb  44987  reuopreuprim  44989  goldbachthlem2  45009  odz2prm2pw  45026  fmtnoprmfac1  45028  fmtnofac2lem  45031  prmdvdsfmtnof1lem2  45048  2pwp1prm  45052  sfprmdvdsmersenne  45066  lighneallem3  45070  requad01  45084  requad2  45086  even3prm2  45182  fppr2odd  45194  fpprwpprb  45203  gbegt5  45224  sbgoldbwt  45240  sbgoldbalt  45244  sbgoldbm  45247  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  bgoldbtbnd  45272  tgblthelfgott  45278  tgoldbach  45280  isomuspgrlem2b  45292  isomuspgrlem2d  45294  isomuspgr  45297  isomgrsym  45299  upgrwlkupwlk  45313  lmod0rng  45437  nzerooringczr  45641  ztprmneprm  45694  ply1mulgsumlem1  45738  ply1mulgsumlem2  45739  lcoel0  45780  linindslinci  45800  lindslinindimp2lem4  45813  lindslinindsimp2lem5  45814  snlindsntor  45823  ldepspr  45825  lincresunit2  45830  fllog2  45925  dignn0ldlem  45959  dignn0flhalflem1  45972  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  itcovalt2  46034  resum2sqorgt0  46066  eenglngeehlnmlem2  46095  rrx2linest  46099  itscnhlc0xyqsol  46122  itsclc0  46128  setrec1lem2  46405  aacllem  46516