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

Theorem com23 72
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 35 . 2  |-  ( ch 
->  ( ( ch  ->  th )  ->  th )
)
31, 2syl9 66 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com3r  73  com13  74  pm2.04  76  pm2.86d  93  impancom  427  dedlem0b  919  3com23  1157  exp3acom23  1362  ax12b  1655  a16g  1885  cbv1h  1918  sbied  1976  sbequi  1999  ax11indn  2134  eqrdav  2282  ralrimdva  2633  ralrimdvva  2638  ceqsalt  2810  vtoclgft  2834  reu6  2954  sbciegft  3021  reuss2  3448  reupick  3452  pwssun  4299  wefrc  4387  tz7.7  4418  ordtr2  4436  onmindif  4482  unizlim  4509  reusv2lem3  4537  reusv3  4542  limsssuc  4641  tfindsg  4651  limomss  4661  findsg  4683  ssrel  4776  ssrelrel  4787  funssres  5294  funcnvuni  5317  fv3  5541  fvmptt  5615  funfvima2  5754  isoini  5835  isopolem  5842  f1oweALT  5851  weniso  5852  f1ocnv2d  6068  frxp  6225  riotasv2dOLD  6350  riotasv3dOLD  6354  onfununi  6358  tfrlem1  6391  tz7.49  6457  omordi  6564  omlimcl  6576  omass  6578  oeordsuc  6592  nnmordi  6629  nnmord  6630  omabs  6645  xpdom2  6957  infensuc  7039  findcard2  7098  findcard3  7100  frfi  7102  xpfi  7128  dffi2  7176  elfiun  7183  ordiso2  7230  ordtypelem7  7239  suc11reg  7320  inf3lem2  7330  noinfep  7360  noinfepOLD  7361  cantnfle  7372  cantnflem1  7391  cantnf  7395  trcl  7410  epfrs  7413  r1sdom  7446  pr2ne  7635  dfac8alem  7656  indcardi  7668  alephordi  7701  dfac12lem3  7771  pwsdompw  7830  cofsmo  7895  cfcoflem  7898  coftr  7899  isf32lem2  7980  isf32lem9  7987  axcc3  8064  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  zorn2lem4  8126  zorn2lem6  8128  zorn2lem7  8129  ttukeylem6  8141  uniimadom  8166  konigthlem  8190  fpwwe2lem8  8259  tskord  8402  tskcard  8403  grupr  8419  gruiin  8432  grudomon  8439  grur1a  8441  nqereu  8553  genpn0  8627  genpcd  8630  distrlem5pr  8651  psslinpr  8655  ltaddpr  8658  ltexprlem3  8662  ltexprlem6  8665  ltapr  8669  prlem936  8671  suplem1pr  8676  axpre-sup  8791  1re  8837  ltletr  8913  lemul12a  9614  divgt0  9624  divge0  9625  lbreu  9704  sup2  9710  infmrcl  9733  bndndx  9964  elnnz  10034  uzindOLD  10106  fzind  10110  fnn0ind  10111  uzwo  10281  uzwoOLD  10282  eqreznegel  10303  lbzbi  10306  zmax  10313  zbtwnre  10314  irradd  10340  irrmul  10341  xrltletr  10488  xrub  10630  supxrunb2  10639  iccid  10701  fzm1  10862  fzrevral  10866  uzindi  11043  le2sq2  11179  sqlecan  11209  facdiv  11300  facwordi  11302  faclbnd  11303  ccatopth2  11463  cau3lem  11838  caubnd  11842  climrlim2  12021  rlimuni  12024  rlimcn2  12064  mulcn2  12069  rlimno1  12127  climcau  12144  caucvg  12151  xpnnenOLD  12488  dvdsle  12574  ndvdssub  12606  gcdcllem1  12690  dvdslegcd  12695  bezoutlem4  12720  coprmdvds  12781  coprmdvds2  12782  prmfac1  12797  pcqcl  12909  prmpwdvds  12951  infpnlem1  12957  joinle  14127  meetle  14134  clatleglb  14230  sylow2blem3  14933  lsmdisj2  14991  frgpnabllem1  15161  dprddisj2  15274  lssssr  15710  lss1d  15720  lspsncv0  15899  znrrg  16519  uniopn  16643  opnnei  16857  neindisj2  16860  restcls  16911  restntr  16912  tgcnp  16983  subbascn  16984  lmcnp  17032  lpcls  17092  cmpsublem  17126  cmpsub  17127  tgcmp  17128  cmpcld  17129  dfcon2  17145  1stcrest  17179  2ndcdisj  17182  1stccnp  17188  kgencn2  17252  txlm  17342  kqreglem1  17432  filin  17549  isfil2  17551  fgss2  17569  fgfil  17570  ufilmax  17602  ufileu  17614  filufint  17615  cfinufil  17623  elfm2  17643  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  flimopn  17670  fbflim2  17672  flffbas  17690  fclsnei  17714  flimfnfcls  17723  fclscmp  17725  ufilcmp  17727  fcfnei  17730  cnpfcf  17736  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem4  17749  divstgplem  17803  tsmsres  17826  tsmsxp  17837  metss  18054  metcnp3  18086  ivthlem2  18812  ivthlem3  18813  ovoliunnul  18866  ovolicc2lem3  18878  dyadmax  18953  itg2le  19094  itgcn  19197  ellimc3  19229  lhop1  19361  dvfsumrlim  19378  fta1g  19553  fta1  19688  aalioulem3  19714  aalioulem4  19715  ulmcaulem  19771  ulmcau  19772  xrlimcnp  20263  cxploglim  20272  jensen  20283  lgsquad2lem2  20598  2sqlem6  20608  rngoueqz  21097  nmoub3i  21351  ipasslem5  21413  htthlem  21497  ocin  21875  spansneleq  22149  spansnss  22150  elspansn4  22152  h1datomi  22160  nmopub2tALT  22489  nmfnleub2  22506  hstel2  22799  cvnbtwn  22866  spansncv2  22873  dmdmd  22880  dmdbr3  22885  dmdbr4  22886  dmdbr5  22888  mdsl0  22890  mdexchi  22915  cvexchlem  22948  atcv1  22960  atomli  22962  atcvatlem  22965  atcvat2i  22967  chirredi  22974  mdsymlem3  22985  mdsymlem4  22986  sumdmdii  22995  sumdmdlem  22998  cdj1i  23013  f1o3d  23037  cvxpcon  23773  ghomf1olem  24001  dedekindle  24083  fundmpss  24122  dfon2lem6  24144  dfon2lem8  24146  dfon2lem9  24147  dfon2  24148  predpo  24184  trpredrec  24241  soseq  24254  wfr3g  24255  wfrlem12  24267  frr3g  24280  frrlem11  24293  nodenselem5  24339  nodenselem7  24341  nodenselem8  24342  nofulllem5  24360  brbtwn2  24533  ax5seglem5  24561  axcontlem4  24595  axcontlem10  24601  colinearxfr  24698  btwnconn1lem11  24720  lineintmo  24780  ordcmp  24886  ee7.2aOLD  24900  oooeqim2  25053  prj1b  25079  prj3  25080  sssu  25141  geme2  25275  dfps2  25289  trran2  25393  trooo  25394  trinv  25395  glmrngo  25482  truni1  25505  truni2  25506  qusp  25542  iscnp4  25563  cmptdst  25568  limptlimpr2lem2  25575  islimrs4  25582  bwt2  25592  lvsovso  25626  supexr  25631  negveud  25668  negveudr  25669  clsmulcv  25682  icccon2  25700  hdrmp  25706  isder  25707  mrdmcd  25794  ismonc  25814  cmpmon  25815  icmpmon  25816  isepic  25824  idsubfun  25858  tartarmap  25888  setiscat  25979  clscnc  26010  pgapspf2  26053  isib2g1a1  26116  isibg1a2  26117  isibg2a  26118  isibg1a3a  26122  isibg1spa  26123  isibg1a5a  26124  bsstr  26128  nbssntr  26129  sgplpte21d  26136  lppotoslem  26143  nbssntrs  26147  trer  26227  elicc3  26228  finminlem  26231  nn0prpwlem  26238  fnessref  26293  comppfsc  26307  neibastop2  26310  fgmin  26319  tailfb  26326  fdc  26455  heibor1lem  26533  ghomco  26573  unichnidl  26656  dmncan1  26701  pell1qrgap  26959  dford3lem1  27119  hbtlem5  27332  symggen  27411  psgnunilem4  27420  sbiota1  27634  funressnfv  27991  usgranloop  28124  usgra1v  28126  nbusgra  28143  3vfriswmgra  28183  1to2vfriswmgra  28184  1to3vfriswmgra  28185  19.41rg  28316  ee223  28406  lshpdisj  29177  lub0N  29379  leat2  29484  hlrelat2  29592  cvrexchlem  29608  cvratlem  29610  atcvrj0  29617  cvrat2  29618  snatpsubN  29939  linepsubN  29941  pmaple  29950  pmapsub  29957  elpaddn0  29989  paddasslem5  30013  trlval2  30352  cdlemn11pre  31400  dihord2pre  31415  mapdordlem2  31827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator