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  414  expcomd  419  impancom  454  a2and  841  dedlem0b  1039  sbequ1  2249  moexexlem  2711  ralrimdvva  3194  ceqsalt  3527  vtoclgft  3553  vtoclgftOLD  3554  sbciegft  3808  reupick  4287  reusv3  5306  sbcop1  5379  propeqop  5397  pwssun  5456  wefrc  5549  ssrel  5657  ssrel2  5659  ssrelrel  5669  ssrelrn  5763  predpo  6166  tz7.7  6217  ordtr2  6235  onmindif  6280  unizlim  6307  funssres  6398  f1ssf1  6646  fvmptt  6788  fveqdmss  6846  fvcofneq  6859  funsndifnop  6913  funfvima2  6993  isoini  7091  isopolem  7098  weniso  7107  f1ocnv2d  7398  limsssuc  7565  tfindsg  7575  limomss  7585  findsg  7609  funcnvuni  7636  f1oweALT  7673  funelss  7746  bropopvvv  7785  bropfvvvvlem  7786  bropfvvvv  7787  f1o2ndf1  7818  frxp  7820  suppfnss  7855  wfrlem12  7966  onfununi  7978  tz7.49  8081  omordi  8192  omlimcl  8204  omass  8206  oeordsuc  8220  nnmordi  8257  nnmord  8258  omabs  8274  xpdom2  8612  infensuc  8695  findcard2  8758  findcard2d  8760  findcard3  8761  frfi  8763  xpfi  8789  fsuppres  8858  dffi2  8887  elfiun  8894  ordiso2  8979  ordtypelem7  8988  suc11reg  9082  inf3lem2  9092  noinfep  9123  cantnfle  9134  cantnflem1  9152  cantnf  9156  trcl  9170  epfrs  9173  r1sdom  9203  updjud  9363  pr2ne  9431  dfac8alem  9455  indcardi  9467  alephordi  9500  dfac12lem3  9571  pwsdompw  9626  cofsmo  9691  cfcoflem  9694  coftr  9695  isf32lem2  9776  isf32lem9  9783  axcc3  9860  domtriomlem  9864  axdc3lem2  9873  axdc3lem4  9875  zorn2lem4  9921  zorn2lem6  9923  zorn2lem7  9924  ttukeylem6  9936  uniimadom  9966  konigthlem  9990  fpwwe2lem8  10059  tskord  10202  tskcard  10203  grupr  10219  gruiin  10232  grudomon  10239  grur1a  10241  genpn0  10425  genpcd  10428  distrlem5pr  10449  psslinpr  10453  ltaddpr  10456  ltexprlem3  10460  ltexprlem6  10463  ltapr  10467  prlem936  10469  suplem1pr  10474  axpre-sup  10591  1re  10641  dedekindle  10804  lemul12a  11498  divgt0  11508  divge0  11509  lbreu  11591  sup2  11597  bndndx  11897  elnnz  11992  nzadd  12031  fzind  12081  fnn0ind  12082  uzwo  12312  lbzbi  12337  zmax  12346  zbtwnre  12347  irradd  12373  irrmul  12374  ledivge1le  12461  xrub  12706  supxrunb2  12714  infmremnf  12737  iccid  12784  uzsubsubfz  12930  fzrevral  12993  elfz0fzfz0  13013  fz0fzelfz0  13014  elfzmlbp  13019  elincfzoext  13096  ssfzoulel  13132  ssfzo12bi  13133  elfzonelfzo  13140  elfznelfzo  13143  elfznelfzob  13144  injresinjlem  13158  fleqceilz  13223  modaddmodup  13303  uzindi  13351  suppssfz  13363  mptnn0fsuppr  13368  le2sq2  13501  sqlecan  13572  facdiv  13648  facwordi  13650  faclbnd  13651  hashimarni  13803  hash2prd  13834  hashle2pr  13836  pr2pwpr  13838  fundmge2nop0  13851  fi1uzind  13856  brfi1indALT  13859  swrdnd2  14017  swrdnnn0nd  14018  swrdnd0  14019  pfxnd0  14050  swrdswrdlem  14066  swrdswrd  14067  ccatopth2  14079  wrd2ind  14085  pfxccatin12lem2a  14089  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12lem3  14094  swrdccat  14097  swrdccat3blem  14101  reuccatpfxs1lem  14108  repswswrd  14146  cshwidxmod  14165  cshwidx0  14168  2cshwcshw  14187  cshwcsh2id  14190  cau3lem  14714  caubnd  14718  climrlim2  14904  rlimcn2  14947  mulcn2  14952  climcau  15027  climbdd  15028  caucvg  15035  modfsummod  15149  p1modz1  15614  dvdsle  15660  dvdsdivcl  15666  ltoddhalfle  15710  halfleoddlt  15711  ndvdssub  15760  gcdcllem1  15848  dvdslegcd  15853  bezoutlem4  15890  dfgcd2  15894  lcmf  15977  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem  15985  lcmfdvdsb  15987  lcmfun  15989  coprmdvds1  15996  divgcdcoprm0  16009  cncongr1  16011  cncongr2  16012  prmfac1  16063  pcqcl  16193  dvdsprmpweqle  16222  oddprmdvds  16239  prmpwdvds  16240  infpnlem1  16246  prmgaplem5  16391  prmgaplem6  16392  prmgaplem7  16393  cshwshashlem1  16429  cictr  17075  initoeu2lem1  17274  initoeu2  17276  clatleglb  17736  lidrididd  17880  mulgaddcom  18251  mulginvcom  18252  cycsubm  18345  cyccom  18346  gsmsymgreqlem2  18559  symggen  18598  psgnunilem4  18625  sylow2blem3  18747  frgpnabllem1  18993  dprddisj2  19161  f1rhm0to0ALT  19494  lmodfopnelem1  19670  lssssr  19725  lss1d  19735  lspsncv0  19918  mplcoe5lem  20248  cply1mul  20462  coe1fzgsumdlem  20469  gsummoncoe1  20472  evl1gsumdlem  20519  znrrg  20712  mamufacex  21000  dmatelnd  21105  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  smatvscl  21133  mavmulsolcl  21160  mdetdiagid  21209  cramerlem3  21298  pmatcoe1fsupp  21309  cpmatacl  21324  cpmatmcllem  21326  mp2pm2mplem4  21417  chpscmat  21450  chfacfisf  21462  chfacfisfcpmat  21463  uniopn  21505  opnnei  21728  neindisj2  21731  restcls  21789  restntr  21790  tgcnp  21861  subbascn  21862  iscnp4  21871  lpcls  21972  cmpsublem  22007  cmpsub  22008  tgcmp  22009  cmpcld  22010  dfconn2  22027  1stcrest  22061  2ndcdisj  22064  1stccnp  22070  comppfsc  22140  kgencn2  22165  txlm  22256  kqreglem1  22349  filin  22462  isfil2  22464  ufilmax  22515  ufileu  22527  filufint  22528  cfinufil  22536  elfm2  22556  rnelfmlem  22560  rnelfm  22561  flimopn  22583  fbflim2  22585  flffbas  22603  fclsnei  22627  flimfnfcls  22636  fclscmp  22638  fcfnei  22643  cnpfcf  22649  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  ptcmplem4  22663  qustgplem  22729  tsmsres  22752  tsmsxp  22763  metss  23118  metcnp3  23150  ovoliunnul  24108  ovolicc2lem3  24120  dyadmax  24199  itg2le  24340  itgcn  24443  ellimc3  24477  lhop1  24611  dvfsumrlim  24628  fta1g  24761  fta1  24897  aalioulem3  24923  aalioulem4  24924  ulmcaulem  24982  ulmcau  24983  logbgcd1irr  25372  xrlimcnp  25546  cxploglim  25555  jensen  25566  lgsqrmodndvds  25929  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem3  25944  lgsquad2lem2  25961  2lgslem1a1  25965  2sqlem6  25999  2sq2  26009  2sqnn  26015  2sqreultblem  26024  brbtwn2  26691  ax5seglem5  26719  axcontlem4  26753  axcontlem10  26759  umgrnloopv  26891  umgrnloop  26893  upgredgpr  26927  numedglnl  26929  usgrausgrb  26954  usgrnloopvALT  26983  usgrnloopALT  26985  usgredg2vlem2  27008  ushgredgedg  27011  ushgredgedgloop  27013  upgrreslem  27086  umgrreslem  27087  nbgr0vtxlem  27137  nbusgrvtxm1  27161  uvtxnbgrvtx  27175  cusgredg  27206  cusgrres  27230  cusgrsize2inds  27235  cusgrfi  27240  fusgrregdegfi  27351  ewlkle  27387  uspgr2wlkeqi  27429  wlklenvclwlkOLD  27437  lfgrwlkprop  27469  lfgrwlknloop  27471  pthdivtx  27510  2pthnloop  27512  upgrwlkdvdelem  27517  upgrspthswlk  27519  usgr2wlkneq  27537  usgr2trlncl  27541  usgr2pthlem  27544  usgr2pth  27545  uspgrn2crct  27586  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0  27599  wlkiswwlks1  27645  wlkiswwlks2  27653  wlkiswwlksupgr2  27655  wwlksnred  27670  wwlksnext  27671  wwlksnextbi  27672  wwlksnextwrd  27675  wwlksnextinj  27677  wwlksnextproplem2  27689  wwlksnextproplem3  27690  wspthsnonn0vne  27696  wspn0  27703  2pthon3v  27722  umgrwwlks2on  27736  elwspths2on  27739  wpthswwlks2on  27740  clwwlk1loop  27766  clwwlkccatlem  27767  umgrclwwlkge2  27769  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem3  27779  clwlkclwwlkf1lem3  27784  clwlkclwwlkfo  27787  clwwisshclwwslemlem  27791  erclwwlkeqlen  27797  erclwwlksym  27799  clwwlkf  27826  clwwlknscsh  27841  erclwwlknsym  27849  clwwlknonex2lem2  27887  clwwlknonex2  27888  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eucrctshift  28022  3vfriswmgr  28057  1to2vfriswmgr  28058  1to3vfriswmgr  28059  n4cyclfrgr  28070  4cyclusnfrgr  28071  frgrnbnb  28072  frgrncvvdeqlem8  28085  frgrwopreg  28102  frgr2wwlk1  28108  frgr2wwlkeqm  28110  2clwwlk2clwwlklem  28125  numclwwlk1lem2fo  28137  wlkl0  28146  numclwlk2lem2f  28156  frgrreggt1  28172  frgrreg  28173  frgrregord013  28174  frgrregord13  28175  frgrogt3nreg  28176  eulplig  28262  nmoub3i  28550  ipasslem5  28612  htthlem  28694  ocin  29073  spansneleq  29347  spansnss  29348  elspansn4  29350  h1datomi  29358  nmopub2tALT  29686  nmfnleub2  29703  hstel2  29996  cvnbtwn  30063  spansncv2  30070  dmdmd  30077  dmdbr3  30082  dmdbr4  30083  dmdbr5  30085  mdsl0  30087  mdexchi  30112  cvexchlem  30145  atcv1  30157  atomli  30159  atcvatlem  30162  atcvat2i  30164  chirredi  30171  mdsymlem3  30182  mdsymlem4  30183  sumdmdii  30192  sumdmdlem  30195  cdj1i  30210  ssrelf  30366  f1o3d  30372  fisshasheq  32352  umgr2cycllem  32387  cvxpconn  32489  satfv0  32605  satfsschain  32611  satfrel  32614  satfdm  32616  satfv0fun  32618  sat1el2xp  32626  gonarlem  32641  goalrlem  32643  satffunlem1lem1  32649  satffunlem2lem1  32651  satffunlem2lem2  32653  satffun  32656  mrsubccat  32765  msubvrs  32807  fundmpss  33009  dfon2lem6  33033  dfon2lem8  33035  dfon2lem9  33036  dfon2  33037  trpredrec  33077  soseq  33096  wzel  33111  frr3g  33121  nosepdmlem  33187  nodenselem8  33195  colinearxfr  33536  btwnconn1lem11  33558  lineintmo  33618  trer  33664  elicc3  33665  finminlem  33666  nn0prpwlem  33670  fnessref  33705  neibastop2  33709  fgmin  33718  tailfb  33725  ordcmp  33795  ee7.2aOLD  33809  bj-cbvalimt  33972  bj-ceqsalt0  34203  bj-ceqsalt1  34204  isbasisrelowllem1  34639  isbasisrelowllem2  34640  relowlpssretop  34648  fvineqsneu  34695  fvineqsneq  34696  wl-mo3t  34827  finixpnum  34892  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  bddiblnc  34977  ftc1anc  34990  fdc  35035  heibor1lem  35102  ghomco  35184  rngoueqz  35233  unichnidl  35324  dmncan1  35369  ax12indn  36094  lshpdisj  36138  lub0N  36340  glb0N  36344  leat2  36445  hlrelat2  36554  cvrexchlem  36570  cvratlem  36572  atcvrj0  36579  cvrat2  36580  snatpsubN  36901  linepsubN  36903  pmaple  36912  pmapsub  36919  elpaddn0  36951  paddasslem5  36975  trlval2  37314  cdlemn11pre  38361  dihord2pre  38376  mapdordlem2  38788  pell1qrgap  39520  dford3lem1  39672  hbtlem5  39777  ntrneiiso  40490  sbiota1  40815  19.41rg  40933  ee223  41017  or2expropbilem1  43316  funressnfv  43327  2reuimp  43363  f1oresf1o2  43539  zm1nn  43551  nltle2tri  43562  el1fzopredsuc  43574  fzoopth  43576  elsetpreimafvssdm  43595  imasetpreimafvbijlemf1  43613  iccpartlt  43633  iccpartgt  43636  iccelpart  43642  icceuelpart  43645  iccpartnel  43647  fargshiftfo  43651  fargshiftfva  43652  lswn0  43653  ich2exprop  43682  prsprel  43698  sprsymrelfolem2  43704  sprsymrelfo  43708  poprelb  43735  reuopreuprim  43737  goldbachthlem2  43757  odz2prm2pw  43774  fmtnoprmfac1  43776  fmtnofac2lem  43779  prmdvdsfmtnof1lem2  43796  2pwp1prm  43800  sfprmdvdsmersenne  43817  lighneallem3  43821  requad01  43835  requad2  43837  even3prm2  43933  fppr2odd  43945  fpprwpprb  43954  gbegt5  43975  sbgoldbwt  43991  sbgoldbalt  43995  sbgoldbm  43998  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  tgblthelfgott  44029  tgoldbach  44031  isomuspgrlem2b  44043  isomuspgrlem2d  44045  isomuspgr  44048  isomgrsym  44050  upgrwlkupwlk  44064  lmod0rng  44188  nzerooringczr  44392  ztprmneprm  44444  ply1mulgsumlem1  44489  ply1mulgsumlem2  44490  lcoel0  44532  linindslinci  44552  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  snlindsntor  44575  ldepspr  44577  lincresunit2  44582  fllog2  44677  dignn0ldlem  44711  dignn0flhalflem1  44724  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  resum2sqorgt0  44745  eenglngeehlnmlem2  44774  rrx2linest  44778  itscnhlc0xyqsol  44801  itsclc0  44807  setrec1lem2  44840  aacllem  44951