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  1372  ax12b  1689  a16g  1950  cbv1h  1983  sbied  2041  sbequi  2064  ax11indn  2200  eqrdav  2357  ralrimdva  2709  ralrimdvva  2714  ceqsalt  2886  vtoclgft  2910  reu6  3030  sbciegft  3097  reuss2  3524  reupick  3528  pwssun  4381  wefrc  4469  tz7.7  4500  ordtr2  4518  onmindif  4564  unizlim  4591  reusv2lem3  4619  reusv3  4624  limsssuc  4723  tfindsg  4733  limomss  4743  findsg  4765  ssrel  4858  ssrelrel  4869  funssres  5376  funcnvuni  5399  fv3  5624  fvmptt  5698  funfvima2  5840  isoini  5922  isopolem  5929  f1oweALT  5938  weniso  5939  f1ocnv2d  6155  frxp  6312  riotasv2dOLD  6437  riotasv3dOLD  6441  onfununi  6445  tfrlem1  6478  tz7.49  6544  omordi  6651  omlimcl  6663  omass  6665  oeordsuc  6679  nnmordi  6716  nnmord  6717  omabs  6732  xpdom2  7045  infensuc  7127  findcard2  7188  findcard3  7190  frfi  7192  xpfi  7218  dffi2  7266  elfiun  7273  ordiso2  7320  ordtypelem7  7329  suc11reg  7410  inf3lem2  7420  noinfep  7450  noinfepOLD  7451  cantnfle  7462  cantnflem1  7481  cantnf  7485  trcl  7500  epfrs  7503  r1sdom  7536  pr2ne  7725  dfac8alem  7746  indcardi  7758  alephordi  7791  dfac12lem3  7861  pwsdompw  7920  cofsmo  7985  cfcoflem  7988  coftr  7989  isf32lem2  8070  isf32lem9  8077  axcc3  8154  domtriomlem  8158  axdc3lem2  8167  axdc3lem4  8169  zorn2lem4  8216  zorn2lem6  8218  zorn2lem7  8219  ttukeylem6  8231  uniimadom  8256  konigthlem  8280  fpwwe2lem8  8349  tskord  8492  tskcard  8493  grupr  8509  gruiin  8522  grudomon  8529  grur1a  8531  nqereu  8643  genpn0  8717  genpcd  8720  distrlem5pr  8741  psslinpr  8745  ltaddpr  8748  ltexprlem3  8752  ltexprlem6  8755  ltapr  8759  prlem936  8761  suplem1pr  8766  axpre-sup  8881  1re  8927  ltletr  9003  lemul12a  9704  divgt0  9714  divge0  9715  lbreu  9794  sup2  9800  infmrcl  9823  bndndx  10056  elnnz  10126  uzindOLD  10198  fzind  10202  fnn0ind  10203  uzwo  10373  uzwoOLD  10374  eqreznegel  10395  lbzbi  10398  zmax  10405  zbtwnre  10406  irradd  10432  irrmul  10433  xrltletr  10580  xrub  10722  supxrunb2  10731  iccid  10793  fzm1  10954  fzrevral  10958  uzindi  11135  le2sq2  11272  sqlecan  11302  facdiv  11393  facwordi  11395  faclbnd  11396  ccatopth2  11559  cau3lem  11934  caubnd  11938  climrlim2  12117  rlimuni  12120  rlimcn2  12160  mulcn2  12165  rlimno1  12223  climcau  12240  climbdd  12241  caucvg  12248  xpnnenOLD  12585  dvdsle  12671  ndvdssub  12703  gcdcllem1  12787  dvdslegcd  12792  bezoutlem4  12817  coprmdvds  12878  coprmdvds2  12879  prmfac1  12894  pcqcl  13006  prmpwdvds  13048  infpnlem1  13054  joinle  14226  meetle  14233  clatleglb  14329  sylow2blem3  15032  lsmdisj2  15090  frgpnabllem1  15260  dprddisj2  15373  lssssr  15809  lss1d  15819  lspsncv0  15998  znrrg  16625  uniopn  16749  opnnei  16963  neindisj2  16966  restcls  17017  restntr  17018  tgcnp  17089  subbascn  17090  lmcnp  17138  lpcls  17198  cmpsublem  17232  cmpsub  17233  tgcmp  17234  cmpcld  17235  dfcon2  17251  1stcrest  17285  2ndcdisj  17288  1stccnp  17294  kgencn2  17358  txlm  17448  kqreglem1  17538  filin  17651  isfil2  17653  fgss2  17671  fgfil  17672  ufilmax  17704  ufileu  17716  filufint  17717  cfinufil  17725  elfm2  17745  rnelfmlem  17749  rnelfm  17750  fmfnfmlem2  17752  fmfnfmlem4  17754  flimopn  17772  fbflim2  17774  flffbas  17792  fclsnei  17816  flimfnfcls  17825  fclscmp  17827  ufilcmp  17829  fcfnei  17832  cnpfcf  17838  alexsubALTlem2  17844  alexsubALTlem3  17845  alexsubALTlem4  17846  alexsubALT  17847  ptcmplem4  17851  divstgplem  17905  tsmsres  17928  tsmsxp  17939  metss  18156  metcnp3  18188  ivthlem2  18916  ivthlem3  18917  ovoliunnul  18970  ovolicc2lem3  18982  dyadmax  19057  itg2le  19198  itgcn  19301  ellimc3  19333  lhop1  19465  dvfsumrlim  19482  fta1g  19657  fta1  19792  aalioulem3  19818  aalioulem4  19819  ulmcaulem  19877  ulmcau  19878  xrlimcnp  20374  cxploglim  20383  jensen  20394  lgsquad2lem2  20710  2sqlem6  20720  rngoueqz  21209  nmoub3i  21465  ipasslem5  21527  htthlem  21611  ocin  21989  spansneleq  22263  spansnss  22264  elspansn4  22266  h1datomi  22274  nmopub2tALT  22603  nmfnleub2  22620  hstel2  22913  cvnbtwn  22980  spansncv2  22987  dmdmd  22994  dmdbr3  22999  dmdbr4  23000  dmdbr5  23002  mdsl0  23004  mdexchi  23029  cvexchlem  23062  atcv1  23074  atomli  23076  atcvatlem  23079  atcvat2i  23081  chirredi  23088  mdsymlem3  23099  mdsymlem4  23100  sumdmdii  23109  sumdmdlem  23112  cdj1i  23127  f1o3d  23245  iscnp4  23447  cvxpcon  24177  ghomf1olem  24405  dedekindle  24489  fundmpss  24680  dfon2lem6  24702  dfon2lem8  24704  dfon2lem9  24705  dfon2  24706  predpo  24742  trpredrec  24799  soseq  24812  wfr3g  24813  wfrlem12  24825  frr3g  24838  frrlem11  24851  nodenselem5  24897  nodenselem7  24899  nodenselem8  24900  nofulllem5  24918  brbtwn2  25092  ax5seglem5  25120  axcontlem4  25154  axcontlem10  25160  colinearxfr  25257  btwnconn1lem11  25279  lineintmo  25339  ordcmp  25445  ee7.2aOLD  25459  bddiblnc  25510  trer  25551  elicc3  25552  finminlem  25555  nn0prpwlem  25562  fnessref  25617  comppfsc  25631  neibastop2  25634  fgmin  25643  tailfb  25650  fdc  25779  heibor1lem  25856  ghomco  25896  unichnidl  25979  dmncan1  26024  pell1qrgap  26282  dford3lem1  26442  hbtlem5  26655  symggen  26734  psgnunilem4  26743  sbiota1  26957  funressnfv  27316  bropopvvv  27435  elfznelfzo  27462  elfznelfzob  27463  injresinjlem  27464  hashle00  27490  brfi1uzind  27497  usgranloop  27553  usgra2edg  27556  usgraedg4  27560  usgra1v  27563  usgraidx2vlem2  27565  usgrafisindb0  27576  usgrafisindb1  27577  usgrares1  27578  nbusgra  27594  cusgrarn  27622  cusgrares  27635  cusgrasize2inds  27640  cusgrafi  27645  sizeusglecusg  27649  usgrnloop  27707  1pthoncl  27728  wlkdvspthlem  27743  wlkdvspth  27744  cyclnspth  27754  fargshiftfo  27761  fargshiftfva  27762  eupatrl  27763  usgrcyclnl1  27764  nvnencycllem  27767  constr3trllem2  27775  4cycl4dv  27791  3vfriswmgra  27838  1to2vfriswmgra  27839  1to3vfriswmgra  27840  3cyclfrgrarn  27846  n4cyclfrgra  27851  4cyclusnfrgra  27852  frgranbnb  27853  frgrancvvdeqlemB  27871  ad5ant13  27974  ad5ant14  27975  ad5ant15  27976  ad5ant23  27977  ad5ant24  27978  ad5ant25  27979  ad5ant245  27980  ad5ant234  27981  ad5ant235  27982  ad5ant134  27986  ad5ant135  27987  ad5ant145  27988  19.41rg  28061  ee223  28157  eel12131  28244  eel32131  28247  3imp231  28353  cbv1hwAUX7  28934  sbiedNEW7  28961  a16gNEW7  28967  sbequiNEW7  28999  cbv1hOLD7  29120  lshpdisj  29246  lub0N  29448  leat2  29553  hlrelat2  29661  cvrexchlem  29677  cvratlem  29679  atcvrj0  29686  cvrat2  29687  snatpsubN  30008  linepsubN  30010  pmaple  30019  pmapsub  30026  elpaddn0  30058  paddasslem5  30082  trlval2  30421  cdlemn11pre  31469  dihord2pre  31484  mapdordlem2  31896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator