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	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
com23	|- ( ph -> ( ch -> ( ps -> th ) ) )

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
2		pm2.27 42	. 2 |- ( ch -> ( ( ch -> th ) -> th ) )
3	1, 2	syl9 77	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

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  107  expcomd  454  impancom  456  a2and  853  dedlem0b  1001  3com23  1271  ad5ant13  1301  ad5ant14  1302  ad5ant15  1303  ad5ant134  1313  ad5ant135  1314  moexex  2541  ralrimdvva  2974  ceqsalt  3228  vtoclgft  3254  vtoclgftOLD  3255  reu6  3395  sbciegft  3466  reupick  3911  reusv3  4876  ralxfrd  4879  ralxfrd2  4884  propeqop  4970  pwssun  5020  wefrc  5108  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  ssrelrn  5315  predpo  5698  tz7.7  5749  ordtr2  5768  onmindif  5815  unizlim  5844  funssres  5930  f1ssf1  6168  fv3  6206  fvmptt  6300  fveqdmss  6354  fvcofneq  6367  funsndifnop  6416  fmptsnd  6435  funfvima2  6493  isoini  6588  isopolem  6595  weniso  6604  f1ocnv2d  6886  limsssuc  7050  tfindsg  7060  limomss  7070  findsg  7093  funcnvuni  7119  f1oweALT  7152  bropopvvv  7255  bropfvvvvlem  7256  bropfvvvv  7257  f1o2ndf1  7285  frxp  7287  suppfnss  7320  wfr3g  7413  wfrlem12  7426  onfununi  7438  tz7.49  7540  omordi  7646  omlimcl  7658  omass  7660  oeordsuc  7674  nnmordi  7711  nnmord  7712  omabs  7727  xpdom2  8055  infensuc  8138  findcard2  8200  findcard2d  8202  findcard3  8203  frfi  8205  xpfi  8231  fsuppres  8300  dffi2  8329  elfiun  8336  ordiso2  8420  ordtypelem7  8429  suc11reg  8516  inf3lem2  8526  noinfep  8557  cantnfle  8568  cantnflem1  8586  cantnf  8590  trcl  8604  epfrs  8607  r1sdom  8637  pr2ne  8828  dfac8alem  8852  indcardi  8864  alephordi  8897  dfac12lem3  8967  pwsdompw  9026  cofsmo  9091  cfcoflem  9094  coftr  9095  isf32lem2  9176  isf32lem9  9183  axcc3  9260  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  zorn2lem4  9321  zorn2lem6  9323  zorn2lem7  9324  ttukeylem6  9336  uniimadom  9366  konigthlem  9390  fpwwe2lem8  9459  tskord  9602  tskcard  9603  grupr  9619  gruiin  9632  grudomon  9639  grur1a  9641  nqereu  9751  genpn0  9825  genpcd  9828  distrlem5pr  9849  psslinpr  9853  ltaddpr  9856  ltexprlem3  9860  ltexprlem6  9863  ltapr  9867  prlem936  9869  suplem1pr  9874  axpre-sup  9990  1re  10039  ltletr  10129  dedekindle  10201  lemul12a  10881  divgt0  10891  divge0  10892  lbreu  10973  sup2  10979  bndndx  11291  elnnz  11387  nzadd  11425  fzind  11475  fnn0ind  11476  uzwo  11751  eqreznegel  11774  lbzbi  11776  zmax  11785  zbtwnre  11786  irradd  11812  irrmul  11813  ledivge1le  11901  xrltletr  11988  xnn0xaddcl  12066  xrub  12142  supxrunb2  12150  infmremnf  12173  iccid  12220  uzsubsubfz  12363  fzrevral  12425  elfz0fzfz0  12444  fz0fzelfz0  12445  elfzmlbp  12450  elincfzoext  12525  elfzodifsumelfzo  12533  ssfzoulel  12562  ssfzo12bi  12563  elfzonelfzo  12570  elfznelfzo  12573  elfznelfzob  12574  injresinjlem  12588  fleqceilz  12653  modaddmodup  12733  uzindi  12781  suppssfz  12794  mptnn0fsuppr  12799  le2sq2  12939  sqlecan  12971  facdiv  13074  facwordi  13076  faclbnd  13077  hashimarni  13228  hash2prd  13257  hashle2pr  13259  pr2pwpr  13261  fundmge2nop0  13274  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdnd2  13433  swrdswrdlem  13459  swrdswrd  13460  ccatopth2  13471  wrd2ind  13477  reuccats1lem  13479  swrdccatin1  13483  swrdccatin12lem2a  13485  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12lem3  13490  swrdccat  13493  swrdccat3blem  13495  repswswrd  13531  cshwidxmod  13549  cshwidx0  13552  2cshwcshw  13571  cshwcsh2id  13574  cau3lem  14094  caubnd  14098  climrlim2  14278  rlimuni  14281  rlimcn2  14321  mulcn2  14326  rlimno1  14384  climcau  14401  climbdd  14402  caucvg  14409  modfsummod  14526  dvdsle  15032  dvdsdivcl  15038  ltoddhalfle  15085  halfleoddlt  15086  ndvdssub  15133  gcdcllem1  15221  dvdslegcd  15226  bezoutlem4  15259  dfgcd2  15263  lcmf  15346  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  lcmfunsnlem  15354  lcmfdvdsb  15356  lcmfun  15358  coprmdvds1  15365  coprmdvds  15366  coprmdvdsOLD  15367  coprmdvds2  15368  divgcdcoprm0  15379  cncongr1  15381  cncongr2  15382  prmfac1  15431  pcqcl  15561  dvdsprmpweqle  15590  oddprmdvds  15607  prmpwdvds  15608  infpnlem1  15614  prmgaplem5  15759  prmgaplem6  15760  prmgaplem7  15761  cshwshashlem1  15802  cictr  16465  initoeu2lem1  16664  initoeu2  16666  clatleglb  17126  mulgaddcom  17564  mulginvcom  17565  gsmsymgrfixlem1  17847  gsmsymgreqlem2  17851  symggen  17890  psgnunilem4  17917  sylow2blem3  18037  lsmdisj2  18095  frgpnabllem1  18276  dprddisj2  18438  f1rhm0to0ALT  18741  lmodfopnelem1  18899  lssssr  18953  lss1d  18963  lspsncv0  19146  mplcoe5lem  19467  cply1mul  19664  coe1fzgsumdlem  19671  gsummoncoe1  19674  evl1gsumdlem  19720  znrrg  19914  mamufacex  20195  dmatelnd  20302  scmataddcl  20322  scmatsubcl  20323  scmatmulcl  20324  smatvscl  20330  mavmulsolcl  20357  mdetdiagid  20406  cramerlem3  20495  pmatcoe1fsupp  20506  cpmatacl  20521  cpmatmcllem  20523  mp2pm2mplem4  20614  chpscmat  20647  chfacfisf  20659  chfacfisfcpmat  20660  uniopn  20702  opnnei  20924  neindisj2  20927  restcls  20985  restntr  20986  tgcnp  21057  subbascn  21058  iscnp4  21067  lmcnp  21108  lpcls  21168  cmpsublem  21202  cmpsub  21203  tgcmp  21204  cmpcld  21205  dfconn2  21222  1stcrest  21256  2ndcdisj  21259  1stccnp  21265  comppfsc  21335  kgencn2  21360  txlm  21451  kqreglem1  21544  filin  21658  isfil2  21660  fgss2  21678  fgfil  21679  ufilmax  21711  ufileu  21723  filufint  21724  cfinufil  21732  elfm2  21752  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  flimopn  21779  fbflim2  21781  flffbas  21799  fclsnei  21823  flimfnfcls  21832  fclscmp  21834  ufilcmp  21836  fcfnei  21839  cnpfcf  21845  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem4  21859  qustgplem  21924  tsmsres  21947  tsmsxp  21958  metss  22313  metcnp3  22345  ivthlem2  23221  ivthlem3  23222  ovoliunnul  23275  ovolicc2lem3  23287  dyadmax  23366  itg2le  23506  itgcn  23609  ellimc3  23643  lhop1  23777  dvfsumrlim  23794  fta1g  23927  fta1  24063  aalioulem3  24089  aalioulem4  24090  ulmcaulem  24148  ulmcau  24149  xrlimcnp  24695  cxploglim  24704  jensen  24715  lgsqrmodndvds  25078  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem3  25093  lgsquad2lem2  25110  2lgslem1a1  25114  2sqlem6  25148  brbtwn2  25785  ax5seglem5  25813  axcontlem4  25847  axcontlem10  25853  umgrnloopv  26001  umgrnloop  26003  umgrislfupgrlem  26017  upgredgpr  26037  numedglnl  26039  usgrausgrb  26064  usgrnloopvALT  26093  usgrnloopALT  26095  uhgr2edg  26100  usgredg2vlem2  26118  ushgredgedg  26121  ushgredgedgloop  26123  upgrreslem  26196  umgrreslem  26197  nbgr0vtxlem  26251  nbusgrvtxm1  26281  uvtxanbgrvtx  26293  cusgredg  26320  cusgrres  26344  cusgrsize2inds  26349  cusgrfi  26354  fusgrregdegfi  26465  ewlkle  26501  upgrewlkle2  26502  uspgr2wlkeqi  26544  wlkv0  26547  wlklenvclwlk  26551  lfgrwlkprop  26584  lfgrwlknloop  26586  pthdivtx  26625  2pthnloop  26627  upgrwlkdvdelem  26632  upgrspthswlk  26634  usgr2wlkneq  26652  usgr2trlncl  26656  usgr2pthlem  26659  usgr2pth  26660  uspgrn2crct  26700  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0  26713  wlkiswwlks1  26753  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wwlksnred  26787  wwlksnext  26788  wwlksnextbi  26789  wwlksnextwrd  26792  wwlksnextinj  26794  wwlksnextproplem2  26805  wwlksnextproplem3  26806  wspthsnonn0vne  26813  2pthon3v  26839  wwlks2onv  26847  umgrwwlks2on  26850  elwspths2on  26853  wpthswwlks2on  26854  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem3  26902  clwwlks1loop  26908  umgrclwwlksge2  26912  clwwlksf  26915  wwlksext2clwwlk  26924  clwwisshclwwslemlem  26926  erclwwlkseqlen  26933  erclwwlkssym  26935  clwwlksnscsh  26940  erclwwlksnsym  26947  clwlksfclwwlk  26962  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eucrctshift  27103  3vfriswmgr  27142  1to2vfriswmgr  27143  1to3vfriswmgr  27144  n4cyclfrgr  27155  4cyclusnfrgr  27156  frgrnbnb  27157  frgrncvvdeqlem8  27170  frgrwopreg  27187  frgr2wwlk1  27193  frgr2wwlkeqm  27195  clwwlkextfrlem1  27208  numclwwlkovf2exlem2  27212  numclwwlkovf2ex  27219  numclwlk1lem2fo  27228  numclwlk2lem2f  27236  numclwwlk8  27250  frgrreggt1  27251  frgrreg  27252  frgrregord013  27253  frgrregord13  27254  frgrogt3nreg  27255  eulplig  27337  nmoub3i  27628  ipasslem5  27690  htthlem  27774  ocin  28155  spansneleq  28429  spansnss  28430  elspansn4  28432  h1datomi  28440  nmopub2tALT  28768  nmfnleub2  28785  hstel2  29078  cvnbtwn  29145  spansncv2  29152  dmdmd  29159  dmdbr3  29164  dmdbr4  29165  dmdbr5  29167  mdsl0  29169  mdexchi  29194  cvexchlem  29227  atcv1  29239  atomli  29241  atcvatlem  29244  atcvat2i  29246  chirredi  29253  mdsymlem3  29264  mdsymlem4  29265  sumdmdii  29274  sumdmdlem  29277  cdj1i  29292  ssrelf  29425  f1o3d  29431  cvxpconn  31224  mrsubccat  31415  msubvrs  31457  fundmpss  31664  dfon2lem6  31693  dfon2lem8  31695  dfon2lem9  31696  dfon2  31697  trpredrec  31738  soseq  31751  wzel  31771  wzelOLD  31772  frr3g  31779  frrlem11  31792  nosepdmlem  31833  nodenselem8  31841  colinearxfr  32182  btwnconn1lem11  32204  lineintmo  32264  trer  32310  elicc3  32311  finminlem  32312  nn0prpwlem  32317  fnessref  32352  neibastop2  32356  fgmin  32365  tailfb  32372  ordcmp  32446  ee7.2aOLD  32460  bj-ceqsalt0  32873  bj-ceqsalt1  32874  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlpssretop  33212  wl-mo3t  33358  finixpnum  33394  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  bddiblnc  33480  ftc1anc  33493  fdc  33541  heibor1lem  33608  ghomco  33690  rngoueqz  33739  unichnidl  33830  dmncan1  33875  ax12indn  34228  lshpdisj  34274  lub0N  34476  glb0N  34480  leat2  34581  hlrelat2  34689  cvrexchlem  34705  cvratlem  34707  atcvrj0  34714  cvrat2  34715  snatpsubN  35036  linepsubN  35038  pmaple  35047  pmapsub  35054  elpaddn0  35086  paddasslem5  35110  trlval2  35450  cdlemn11pre  36499  dihord2pre  36514  mapdordlem2  36926  pell1qrgap  37438  dford3lem1  37593  hbtlem5  37698  ntrneiiso  38389  sbiota1  38635  19.41rg  38766  ee223  38859  funressnfv  41208  zm1nn  41316  nltle2tri  41323  el1fzopredsuc  41335  fzoopth  41337  iccpartlt  41360  iccpartgt  41363  iccelpart  41369  icceuelpart  41372  iccpartnel  41374  fargshiftfo  41378  fargshiftfva  41379  lswn0  41380  pfxccatin12lem2  41424  reuccatpfxs1lem  41433  goldbachthlem2  41458  odz2prm2pw  41475  fmtnoprmfac1  41477  fmtnofac2lem  41480  prmdvdsfmtnof1lem2  41497  2pwp1prm  41503  sfprmdvdsmersenne  41520  lighneallem3  41524  even3prm2  41628  gbegt5  41649  sbgoldbwt  41665  sbgoldbalt  41669  sbgoldbm  41672  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgblthelfgott  41703  tgoldbach  41705  tgblthelfgottOLD  41709  tgoldbachOLD  41712  upgrwlkupwlk  41721  prsprel  41737  sprsymrelfolem2  41743  sprsymrelfo  41747  lmod0rng  41868  nzerooringczr  42072  ztprmneprm  42125  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  lcoel0  42217  linindslinci  42237  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  snlindsntor  42260  ldepspr  42262  lincresunit2  42267  fllog2  42362  dignn0ldlem  42396  dignn0flhalflem1  42409  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  setrec1lem2  42435  aacllem  42547