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  sbied  2151  ax11indn  2274  eqrdav  2437  ralrimdva  2798  ralrimdvva  2803  ceqsalt  2980  vtoclgft  3004  reu6  3125  sbciegft  3193  reuss2  3623  reupick  3627  pwssun  4492  wefrc  4579  tz7.7  4610  ordtr2  4628  onmindif  4674  unizlim  4701  reusv2lem3  4729  reusv3  4734  limsssuc  4833  tfindsg  4843  limomss  4853  findsg  4875  ssrel  4967  ssrel2  4969  ssrelrel  4979  funssres  5496  funcnvuni  5521  fv3  5747  fvmptt  5823  funfvima2  5977  isoini  6061  isopolem  6068  f1oweALT  6077  weniso  6078  f1ocnv2d  6298  bropopvvv  6429  f1o2ndf1  6457  frxp  6459  riotasv2dOLD  6598  riotasv3dOLD  6602  onfununi  6606  tfrlem1  6639  tz7.49  6705  omordi  6812  omlimcl  6824  omass  6826  oeordsuc  6840  nnmordi  6877  nnmord  6878  omabs  6893  xpdom2  7206  infensuc  7288  findcard2  7351  findcard3  7353  frfi  7355  xpfi  7381  dffi2  7431  elfiun  7438  ordiso2  7487  ordtypelem7  7496  suc11reg  7577  inf3lem2  7587  noinfep  7617  noinfepOLD  7618  cantnfle  7629  cantnflem1  7648  cantnf  7652  trcl  7667  epfrs  7670  r1sdom  7703  pr2ne  7894  dfac8alem  7915  indcardi  7927  alephordi  7960  dfac12lem3  8030  pwsdompw  8089  cofsmo  8154  cfcoflem  8157  coftr  8158  isf32lem2  8239  isf32lem9  8246  axcc3  8323  domtriomlem  8327  axdc3lem2  8336  axdc3lem4  8338  zorn2lem4  8384  zorn2lem6  8386  zorn2lem7  8387  ttukeylem6  8399  uniimadom  8424  konigthlem  8448  fpwwe2lem8  8517  tskord  8660  tskcard  8661  grupr  8677  gruiin  8690  grudomon  8697  grur1a  8699  nqereu  8811  genpn0  8885  genpcd  8888  distrlem5pr  8909  psslinpr  8913  ltaddpr  8916  ltexprlem3  8920  ltexprlem6  8923  ltapr  8927  prlem936  8929  suplem1pr  8934  axpre-sup  9049  1re  9095  ltletr  9171  lemul12a  9873  divgt0  9883  divge0  9884  lbreu  9963  sup2  9969  infmrcl  9992  bndndx  10225  elnnz  10297  uzindOLD  10369  fzind  10373  fnn0ind  10374  uzwo  10544  uzwoOLD  10545  eqreznegel  10566  lbzbi  10569  zmax  10576  zbtwnre  10577  irradd  10603  irrmul  10604  xrltletr  10752  xrub  10895  supxrunb2  10904  iccid  10966  fzm1  11132  fzrevral  11136  elfznelfzo  11197  elfznelfzob  11198  injresinjlem  11204  uzindi  11325  le2sq2  11462  sqlecan  11492  facdiv  11583  facwordi  11585  faclbnd  11586  hashle00  11674  brfi1uzind  11720  ccatopth2  11782  cau3lem  12163  caubnd  12167  climrlim2  12346  rlimuni  12349  rlimcn2  12389  mulcn2  12394  rlimno1  12452  climcau  12469  climbdd  12470  caucvg  12477  xpnnenOLD  12814  dvdsle  12900  ndvdssub  12932  gcdcllem1  13016  dvdslegcd  13021  bezoutlem4  13046  coprmdvds  13107  coprmdvds2  13108  prmfac1  13123  pcqcl  13235  prmpwdvds  13277  infpnlem1  13283  joinle  14455  meetle  14462  clatleglb  14558  sylow2blem3  15261  lsmdisj2  15319  frgpnabllem1  15489  dprddisj2  15602  lssssr  16034  lss1d  16044  lspsncv0  16223  znrrg  16851  uniopn  16975  opnnei  17189  neindisj2  17192  restcls  17250  restntr  17251  tgcnp  17322  subbascn  17323  iscnp4  17332  lmcnp  17373  lpcls  17433  cmpsublem  17467  cmpsub  17468  tgcmp  17469  cmpcld  17470  bwth  17478  dfcon2  17487  1stcrest  17521  2ndcdisj  17524  1stccnp  17530  kgencn2  17594  txlm  17685  kqreglem1  17778  filin  17891  isfil2  17893  fgss2  17911  fgfil  17912  ufilmax  17944  ufileu  17956  filufint  17957  cfinufil  17965  elfm2  17985  rnelfmlem  17989  rnelfm  17990  fmfnfmlem2  17992  fmfnfmlem4  17994  flimopn  18012  fbflim2  18014  flffbas  18032  fclsnei  18056  flimfnfcls  18065  fclscmp  18067  ufilcmp  18069  fcfnei  18072  cnpfcf  18078  alexsubALTlem2  18084  alexsubALTlem3  18085  alexsubALTlem4  18086  alexsubALT  18087  ptcmplem4  18091  divstgplem  18155  tsmsres  18178  tsmsxp  18189  metss  18543  metcnp3  18575  ivthlem2  19354  ivthlem3  19355  ovoliunnul  19408  ovolicc2lem3  19420  dyadmax  19495  itg2le  19634  itgcn  19737  ellimc3  19771  lhop1  19903  dvfsumrlim  19920  fta1g  20095  fta1  20230  aalioulem3  20256  aalioulem4  20257  ulmcaulem  20315  ulmcau  20316  xrlimcnp  20812  cxploglim  20821  jensen  20832  lgsquad2lem2  21148  2sqlem6  21158  usgranloopv  21403  usgranloop  21404  usgra2edg  21407  usgraedg4  21411  usgra1v  21414  usgraidx2vlem2  21416  usgrafisindb0  21427  usgrafisindb1  21428  usgrares1  21429  cusgrarn  21473  cusgrares  21486  cusgrasize2inds  21491  cusgrafi  21496  sizeusglecusg  21500  usgrnloop  21568  1pthoncl  21597  wlkdvspthlem  21612  wlkdvspth  21613  cyclnspth  21623  fargshiftfo  21630  fargshiftfva  21631  usgrcyclnl1  21632  nvnencycllem  21635  constr3trllem2  21643  4cycl4dv  21659  eupatrl  21695  rngoueqz  22023  nmoub3i  22279  ipasslem5  22341  htthlem  22425  ocin  22803  spansneleq  23077  spansnss  23078  elspansn4  23080  h1datomi  23088  nmopub2tALT  23417  nmfnleub2  23434  hstel2  23727  cvnbtwn  23794  spansncv2  23801  dmdmd  23808  dmdbr3  23813  dmdbr4  23814  dmdbr5  23816  mdsl0  23818  mdexchi  23843  cvexchlem  23876  atcv1  23888  atomli  23890  atcvatlem  23893  atcvat2i  23895  chirredi  23902  mdsymlem3  23913  mdsymlem4  23914  sumdmdii  23923  sumdmdlem  23926  cdj1i  23941  f1o3d  24046  cvxpcon  24934  ghomf1olem  25110  dedekindle  25193  fundmpss  25395  dfon2lem6  25420  dfon2lem8  25422  dfon2lem9  25423  dfon2  25424  predpo  25464  trpredrec  25521  soseq  25534  wfr3g  25542  wfrlem12  25554  wzel  25580  frr3g  25586  frrlem11  25599  nodenselem5  25645  nodenselem7  25647  nodenselem8  25648  nofulllem5  25666  brbtwn2  25849  ax5seglem5  25877  axcontlem4  25911  axcontlem10  25917  colinearxfr  26014  btwnconn1lem11  26036  lineintmo  26096  ordcmp  26202  ee7.2aOLD  26216  bddiblnc  26289  ftc1anc  26302  trer  26333  elicc3  26334  finminlem  26335  nn0prpwlem  26339  fnessref  26387  comppfsc  26401  neibastop2  26404  fgmin  26413  tailfb  26420  fdc  26463  heibor1lem  26532  ghomco  26572  unichnidl  26655  dmncan1  26700  pell1qrgap  26951  dford3lem1  27111  hbtlem5  27323  symggen  27402  psgnunilem4  27411  sbiota1  27625  funressnfv  27982  ralxfrd2  28087  elovmpt3rab1  28107  uzletr  28126  elfzmlbp  28130  elfz0fzfz0  28137  fz0fzelfz0  28141  elfzonelfzo  28155  el2fzo  28161  fzoopth  28162  hashimarni  28187  swrdnd  28216  swrdvalodmlem1  28221  swrdvalodm2  28222  swrdvalodm  28223  swrd0swrd  28231  swrdswrdlem  28232  swrdswrd  28233  swrdccatin1  28239  swrdccatin12lem3a  28242  swrdccatin2  28244  swrdccatin12lem3  28246  swrdccatin12lem4  28247  swrdccat  28250  swrdccat3blem  28252  2cshw1lem2  28283  2cshwmod  28291  lswrdn0  28294  cshweqdif2s  28305  cshweqrep  28308  cshwssizelem1a  28313  cshwssizelem2  28315  cshwssizelem3  28316  usgra2wlkspthlem2  28345  usgra2pthlem1  28348  wwlknimp  28369  wlkiswwlk2  28379  el2wlkonot  28401  usg2wotspth  28416  usg2spthonot  28420  usg2spthonot0  28421  usgfiregdegfi  28426  nbhashuvtx1  28431  3vfriswmgra  28469  1to2vfriswmgra  28470  1to3vfriswmgra  28471  3cyclfrgrarn  28477  n4cyclfrgra  28482  4cyclusnfrgra  28483  frgranbnb  28484  frgrancvvdeqlemB  28501  frg2wot1  28520  frg2woteqm  28522  frg2woteq  28523  usg2spot2nb  28528  2spotmdisj  28531  usgreghash2spot  28532  frgregordn0  28533  ad5ant13  28621  ad5ant14  28622  ad5ant15  28623  ad5ant134  28633  ad5ant135  28634  ad5ant145  28635  19.41rg  28711  ee223  28809  cbv1hwAUX7  29585  sbiedNEW7  29614  a16gNEW7  29620  sbequiNEW7  29653  cbv1hOLD7  29793  lshpdisj  29859  lub0N  30061  leat2  30166  hlrelat2  30274  cvrexchlem  30290  cvratlem  30292  atcvrj0  30299  cvrat2  30300  snatpsubN  30621  linepsubN  30623  pmaple  30632  pmapsub  30639  elpaddn0  30671  paddasslem5  30695  trlval2  31034  cdlemn11pre  32082  dihord2pre  32097  mapdordlem2  32509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator