MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com23 Structured version   Unicode version

Theorem com23 75
Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (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
StepHypRef Expression
1 com3.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
2 pm2.27 38 . 2  |-  ( ch 
->  ( ( ch  ->  th )  ->  th )
)
31, 2syl9 69 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com3r  76  com13  77  pm2.04  79  pm2.86d  96  impancom  429  dedlem0b  921  3com23  1160  exp3acom23  1382  cbv1hOLD  1976  a16gOLD  2050  sbequiOLD  2116  sbiedOLD  2153  ax11indn  2274  eqrdav  2437  ralrimdva  2798  ralrimdvva  2803  ceqsalt  2980  vtoclgft  3004  reu6  3125  sbciegft  3193  reuss2  3623  reupick  3627  pwssun  4491  wefrc  4578  tz7.7  4609  ordtr2  4627  onmindif  4673  unizlim  4700  reusv2lem3  4728  reusv3  4733  limsssuc  4832  tfindsg  4842  limomss  4852  findsg  4874  ssrel  4966  ssrel2  4968  ssrelrel  4978  funssres  5495  funcnvuni  5520  fv3  5746  fvmptt  5822  funfvima2  5976  isoini  6060  isopolem  6067  f1oweALT  6076  weniso  6077  f1ocnv2d  6297  bropopvvv  6428  f1o2ndf1  6456  frxp  6458  riotasv2dOLD  6597  riotasv3dOLD  6601  onfununi  6605  tfrlem1  6638  tz7.49  6704  omordi  6811  omlimcl  6823  omass  6825  oeordsuc  6839  nnmordi  6876  nnmord  6877  omabs  6892  xpdom2  7205  infensuc  7287  findcard2  7350  findcard3  7352  frfi  7354  xpfi  7380  dffi2  7430  elfiun  7437  ordiso2  7486  ordtypelem7  7495  suc11reg  7576  inf3lem2  7586  noinfep  7616  noinfepOLD  7617  cantnfle  7628  cantnflem1  7647  cantnf  7651  trcl  7666  epfrs  7669  r1sdom  7702  pr2ne  7891  dfac8alem  7912  indcardi  7924  alephordi  7957  dfac12lem3  8027  pwsdompw  8086  cofsmo  8151  cfcoflem  8154  coftr  8155  isf32lem2  8236  isf32lem9  8243  axcc3  8320  domtriomlem  8324  axdc3lem2  8333  axdc3lem4  8335  zorn2lem4  8381  zorn2lem6  8383  zorn2lem7  8384  ttukeylem6  8396  uniimadom  8421  konigthlem  8445  fpwwe2lem8  8514  tskord  8657  tskcard  8658  grupr  8674  gruiin  8687  grudomon  8694  grur1a  8696  nqereu  8808  genpn0  8882  genpcd  8885  distrlem5pr  8906  psslinpr  8910  ltaddpr  8913  ltexprlem3  8917  ltexprlem6  8920  ltapr  8924  prlem936  8926  suplem1pr  8931  axpre-sup  9046  1re  9092  ltletr  9168  lemul12a  9870  divgt0  9880  divge0  9881  lbreu  9960  sup2  9966  infmrcl  9989  bndndx  10222  elnnz  10294  uzindOLD  10366  fzind  10370  fnn0ind  10371  uzwo  10541  uzwoOLD  10542  eqreznegel  10563  lbzbi  10566  zmax  10573  zbtwnre  10574  irradd  10600  irrmul  10601  xrltletr  10749  xrub  10892  supxrunb2  10901  iccid  10963  fzm1  11129  fzrevral  11133  elfznelfzo  11194  elfznelfzob  11195  injresinjlem  11201  uzindi  11322  le2sq2  11459  sqlecan  11489  facdiv  11580  facwordi  11582  faclbnd  11583  hashle00  11671  brfi1uzind  11717  ccatopth2  11779  cau3lem  12160  caubnd  12164  climrlim2  12343  rlimuni  12346  rlimcn2  12386  mulcn2  12391  rlimno1  12449  climcau  12466  climbdd  12467  caucvg  12474  xpnnenOLD  12811  dvdsle  12897  ndvdssub  12929  gcdcllem1  13013  dvdslegcd  13018  bezoutlem4  13043  coprmdvds  13104  coprmdvds2  13105  prmfac1  13120  pcqcl  13232  prmpwdvds  13274  infpnlem1  13280  joinle  14452  meetle  14459  clatleglb  14555  sylow2blem3  15258  lsmdisj2  15316  frgpnabllem1  15486  dprddisj2  15599  lssssr  16031  lss1d  16041  lspsncv0  16220  znrrg  16848  uniopn  16972  opnnei  17186  neindisj2  17189  restcls  17247  restntr  17248  tgcnp  17319  subbascn  17320  iscnp4  17329  lmcnp  17370  lpcls  17430  cmpsublem  17464  cmpsub  17465  tgcmp  17466  cmpcld  17467  bwth  17475  dfcon2  17484  1stcrest  17518  2ndcdisj  17521  1stccnp  17527  kgencn2  17591  txlm  17682  kqreglem1  17775  filin  17888  isfil2  17890  fgss2  17908  fgfil  17909  ufilmax  17941  ufileu  17953  filufint  17954  cfinufil  17962  elfm2  17982  rnelfmlem  17986  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem4  17991  flimopn  18009  fbflim2  18011  flffbas  18029  fclsnei  18053  flimfnfcls  18062  fclscmp  18064  ufilcmp  18066  fcfnei  18069  cnpfcf  18075  alexsubALTlem2  18081  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  ptcmplem4  18088  divstgplem  18152  tsmsres  18175  tsmsxp  18186  metss  18540  metcnp3  18572  ivthlem2  19351  ivthlem3  19352  ovoliunnul  19405  ovolicc2lem3  19417  dyadmax  19492  itg2le  19633  itgcn  19736  ellimc3  19768  lhop1  19900  dvfsumrlim  19917  fta1g  20092  fta1  20227  aalioulem3  20253  aalioulem4  20254  ulmcaulem  20312  ulmcau  20313  xrlimcnp  20809  cxploglim  20818  jensen  20829  lgsquad2lem2  21145  2sqlem6  21155  usgranloopv  21400  usgranloop  21401  usgra2edg  21404  usgraedg4  21408  usgra1v  21411  usgraidx2vlem2  21413  usgrafisindb0  21424  usgrafisindb1  21425  usgrares1  21426  cusgrarn  21470  cusgrares  21483  cusgrasize2inds  21488  cusgrafi  21493  sizeusglecusg  21497  usgrnloop  21565  1pthoncl  21594  wlkdvspthlem  21609  wlkdvspth  21610  cyclnspth  21620  fargshiftfo  21627  fargshiftfva  21628  usgrcyclnl1  21629  nvnencycllem  21632  constr3trllem2  21640  4cycl4dv  21656  eupatrl  21692  rngoueqz  22020  nmoub3i  22276  ipasslem5  22338  htthlem  22422  ocin  22800  spansneleq  23074  spansnss  23075  elspansn4  23077  h1datomi  23085  nmopub2tALT  23414  nmfnleub2  23431  hstel2  23724  cvnbtwn  23791  spansncv2  23798  dmdmd  23805  dmdbr3  23810  dmdbr4  23811  dmdbr5  23813  mdsl0  23815  mdexchi  23840  cvexchlem  23873  atcv1  23885  atomli  23887  atcvatlem  23890  atcvat2i  23892  chirredi  23899  mdsymlem3  23910  mdsymlem4  23911  sumdmdii  23920  sumdmdlem  23923  cdj1i  23938  f1o3d  24043  cvxpcon  24931  ghomf1olem  25107  dedekindle  25190  fundmpss  25392  dfon2lem6  25417  dfon2lem8  25419  dfon2lem9  25420  dfon2  25421  predpo  25461  trpredrec  25518  soseq  25531  wfr3g  25539  wfrlem12  25551  wzel  25577  frr3g  25583  frrlem11  25596  nodenselem5  25642  nodenselem7  25644  nodenselem8  25645  nofulllem5  25663  brbtwn2  25846  ax5seglem5  25874  axcontlem4  25908  axcontlem10  25914  colinearxfr  26011  btwnconn1lem11  26033  lineintmo  26093  ordcmp  26199  ee7.2aOLD  26213  bddiblnc  26277  ftc1anc  26290  trer  26321  elicc3  26322  finminlem  26323  nn0prpwlem  26327  fnessref  26375  comppfsc  26389  neibastop2  26392  fgmin  26401  tailfb  26408  fdc  26451  heibor1lem  26520  ghomco  26560  unichnidl  26643  dmncan1  26688  pell1qrgap  26939  dford3lem1  27099  hbtlem5  27311  symggen  27390  psgnunilem4  27399  sbiota1  27613  funressnfv  27970  ralxfrd2  28075  elovmpt3rab1  28095  uzletr  28114  elfzmlbp  28118  elfz0fzfz0  28125  fz0fzelfz0  28129  elfzonelfzo  28143  el2fzo  28149  fzoopth  28150  hashimarni  28175  swrdnd  28204  swrdvalodmlem1  28209  swrdvalodm2  28210  swrdvalodm  28211  swrd0swrd  28219  swrdswrdlem  28220  swrdswrd  28221  swrdccatin1  28227  swrdccatin12lem3a  28230  swrdccatin2  28232  swrdccatin12lem3  28234  swrdccatin12lem4  28235  swrdccat  28238  swrdccat3blem  28240  2cshw1lem2  28271  2cshwmod  28279  lswrdn0  28282  cshweqdif2s  28293  cshweqrep  28296  cshwssizelem1a  28301  cshwssizelem2  28303  cshwssizelem3  28304  usgra2wlkspthlem2  28333  usgra2pthlem1  28336  wwlknimp  28357  wlkiswwlk2  28367  el2wlkonot  28389  usg2wotspth  28404  usg2spthonot  28408  usg2spthonot0  28409  usgfiregdegfi  28414  nbhashuvtx1  28419  3vfriswmgra  28457  1to2vfriswmgra  28458  1to3vfriswmgra  28459  3cyclfrgrarn  28465  n4cyclfrgra  28470  4cyclusnfrgra  28471  frgranbnb  28472  frgrancvvdeqlemB  28489  frg2wot1  28508  frg2woteqm  28510  frg2woteq  28511  usg2spot2nb  28516  2spotmdisj  28519  usgreghash2spot  28520  frgregordn0  28521  ad5ant13  28609  ad5ant14  28610  ad5ant15  28611  ad5ant134  28621  ad5ant135  28622  ad5ant145  28623  19.41rg  28699  ee223  28797  cbv1hwAUX7  29573  sbiedNEW7  29602  a16gNEW7  29608  sbequiNEW7  29641  cbv1hOLD7  29781  lshpdisj  29847  lub0N  30049  leat2  30154  hlrelat2  30262  cvrexchlem  30278  cvratlem  30280  atcvrj0  30287  cvrat2  30288  snatpsubN  30609  linepsubN  30611  pmaple  30620  pmapsub  30627  elpaddn0  30659  paddasslem5  30683  trlval2  31022  cdlemn11pre  32070  dihord2pre  32085  mapdordlem2  32497
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator