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

Theorem com23 74
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 37 . 2  |-  ( ch 
->  ( ( ch  ->  th )  ->  th )
)
31, 2syl9 68 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com3r  75  com13  76  pm2.04  78  pm2.86d  95  impancom  428  dedlem0b  920  3com23  1159  exp3acom23  1381  cbv1hOLD  1975  a16gOLD  2049  sbiedOLD  2124  sbequiOLD  2137  ax11indn  2271  eqrdav  2434  ralrimdva  2788  ralrimdvva  2793  ceqsalt  2970  vtoclgft  2994  reu6  3115  sbciegft  3183  reuss2  3613  reupick  3617  pwssun  4481  wefrc  4568  tz7.7  4599  ordtr2  4617  onmindif  4663  unizlim  4690  reusv2lem3  4718  reusv3  4723  limsssuc  4822  tfindsg  4832  limomss  4842  findsg  4864  ssrel  4956  ssrel2  4958  ssrelrel  4968  funssres  5485  funcnvuni  5510  fv3  5736  fvmptt  5812  funfvima2  5966  isoini  6050  isopolem  6057  f1oweALT  6066  weniso  6067  f1ocnv2d  6287  bropopvvv  6418  f1o2ndf1  6446  frxp  6448  riotasv2dOLD  6587  riotasv3dOLD  6591  onfununi  6595  tfrlem1  6628  tz7.49  6694  omordi  6801  omlimcl  6813  omass  6815  oeordsuc  6829  nnmordi  6866  nnmord  6867  omabs  6882  xpdom2  7195  infensuc  7277  findcard2  7340  findcard3  7342  frfi  7344  xpfi  7370  dffi2  7420  elfiun  7427  ordiso2  7476  ordtypelem7  7485  suc11reg  7566  inf3lem2  7576  noinfep  7606  noinfepOLD  7607  cantnfle  7618  cantnflem1  7637  cantnf  7641  trcl  7656  epfrs  7659  r1sdom  7692  pr2ne  7881  dfac8alem  7902  indcardi  7914  alephordi  7947  dfac12lem3  8017  pwsdompw  8076  cofsmo  8141  cfcoflem  8144  coftr  8145  isf32lem2  8226  isf32lem9  8233  axcc3  8310  domtriomlem  8314  axdc3lem2  8323  axdc3lem4  8325  zorn2lem4  8371  zorn2lem6  8373  zorn2lem7  8374  ttukeylem6  8386  uniimadom  8411  konigthlem  8435  fpwwe2lem8  8504  tskord  8647  tskcard  8648  grupr  8664  gruiin  8677  grudomon  8684  grur1a  8686  nqereu  8798  genpn0  8872  genpcd  8875  distrlem5pr  8896  psslinpr  8900  ltaddpr  8903  ltexprlem3  8907  ltexprlem6  8910  ltapr  8914  prlem936  8916  suplem1pr  8921  axpre-sup  9036  1re  9082  ltletr  9158  lemul12a  9860  divgt0  9870  divge0  9871  lbreu  9950  sup2  9956  infmrcl  9979  bndndx  10212  elnnz  10284  uzindOLD  10356  fzind  10360  fnn0ind  10361  uzwo  10531  uzwoOLD  10532  eqreznegel  10553  lbzbi  10556  zmax  10563  zbtwnre  10564  irradd  10590  irrmul  10591  xrltletr  10739  xrub  10882  supxrunb2  10891  iccid  10953  fzm1  11119  fzrevral  11123  elfznelfzo  11184  elfznelfzob  11185  injresinjlem  11191  uzindi  11312  le2sq2  11449  sqlecan  11479  facdiv  11570  facwordi  11572  faclbnd  11573  hashle00  11661  brfi1uzind  11707  ccatopth2  11769  cau3lem  12150  caubnd  12154  climrlim2  12333  rlimuni  12336  rlimcn2  12376  mulcn2  12381  rlimno1  12439  climcau  12456  climbdd  12457  caucvg  12464  xpnnenOLD  12801  dvdsle  12887  ndvdssub  12919  gcdcllem1  13003  dvdslegcd  13008  bezoutlem4  13033  coprmdvds  13094  coprmdvds2  13095  prmfac1  13110  pcqcl  13222  prmpwdvds  13264  infpnlem1  13270  joinle  14442  meetle  14449  clatleglb  14545  sylow2blem3  15248  lsmdisj2  15306  frgpnabllem1  15476  dprddisj2  15589  lssssr  16021  lss1d  16031  lspsncv0  16210  znrrg  16838  uniopn  16962  opnnei  17176  neindisj2  17179  restcls  17237  restntr  17238  tgcnp  17309  subbascn  17310  iscnp4  17319  lmcnp  17360  lpcls  17420  cmpsublem  17454  cmpsub  17455  tgcmp  17456  cmpcld  17457  bwth  17465  dfcon2  17474  1stcrest  17508  2ndcdisj  17511  1stccnp  17517  kgencn2  17581  txlm  17672  kqreglem1  17765  filin  17878  isfil2  17880  fgss2  17898  fgfil  17899  ufilmax  17931  ufileu  17943  filufint  17944  cfinufil  17952  elfm2  17972  rnelfmlem  17976  rnelfm  17977  fmfnfmlem2  17979  fmfnfmlem4  17981  flimopn  17999  fbflim2  18001  flffbas  18019  fclsnei  18043  flimfnfcls  18052  fclscmp  18054  ufilcmp  18056  fcfnei  18059  cnpfcf  18065  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALTlem4  18073  alexsubALT  18074  ptcmplem4  18078  divstgplem  18142  tsmsres  18165  tsmsxp  18176  metss  18530  metcnp3  18562  ivthlem2  19341  ivthlem3  19342  ovoliunnul  19395  ovolicc2lem3  19407  dyadmax  19482  itg2le  19623  itgcn  19726  ellimc3  19758  lhop1  19890  dvfsumrlim  19907  fta1g  20082  fta1  20217  aalioulem3  20243  aalioulem4  20244  ulmcaulem  20302  ulmcau  20303  xrlimcnp  20799  cxploglim  20808  jensen  20819  lgsquad2lem2  21135  2sqlem6  21145  usgranloopv  21390  usgranloop  21391  usgra2edg  21394  usgraedg4  21398  usgra1v  21401  usgraidx2vlem2  21403  usgrafisindb0  21414  usgrafisindb1  21415  usgrares1  21416  cusgrarn  21460  cusgrares  21473  cusgrasize2inds  21478  cusgrafi  21483  sizeusglecusg  21487  usgrnloop  21555  1pthoncl  21584  wlkdvspthlem  21599  wlkdvspth  21600  cyclnspth  21610  fargshiftfo  21617  fargshiftfva  21618  usgrcyclnl1  21619  nvnencycllem  21622  constr3trllem2  21630  4cycl4dv  21646  eupatrl  21682  rngoueqz  22010  nmoub3i  22266  ipasslem5  22328  htthlem  22412  ocin  22790  spansneleq  23064  spansnss  23065  elspansn4  23067  h1datomi  23075  nmopub2tALT  23404  nmfnleub2  23421  hstel2  23714  cvnbtwn  23781  spansncv2  23788  dmdmd  23795  dmdbr3  23800  dmdbr4  23801  dmdbr5  23803  mdsl0  23805  mdexchi  23830  cvexchlem  23863  atcv1  23875  atomli  23877  atcvatlem  23880  atcvat2i  23882  chirredi  23889  mdsymlem3  23900  mdsymlem4  23901  sumdmdii  23910  sumdmdlem  23913  cdj1i  23928  f1o3d  24033  cvxpcon  24921  ghomf1olem  25097  dedekindle  25180  fundmpss  25382  dfon2lem6  25407  dfon2lem8  25409  dfon2lem9  25410  dfon2  25411  predpo  25451  trpredrec  25508  soseq  25521  wfr3g  25529  wfrlem12  25541  wzel  25567  frr3g  25573  frrlem11  25586  nodenselem5  25632  nodenselem7  25634  nodenselem8  25635  nofulllem5  25653  brbtwn2  25836  ax5seglem5  25864  axcontlem4  25898  axcontlem10  25904  colinearxfr  26001  btwnconn1lem11  26023  lineintmo  26083  ordcmp  26189  ee7.2aOLD  26203  bddiblnc  26265  trer  26300  elicc3  26301  finminlem  26302  nn0prpwlem  26306  fnessref  26354  comppfsc  26368  neibastop2  26371  fgmin  26380  tailfb  26387  fdc  26430  heibor1lem  26499  ghomco  26539  unichnidl  26622  dmncan1  26667  pell1qrgap  26918  dford3lem1  27078  hbtlem5  27290  symggen  27369  psgnunilem4  27378  sbiota1  27592  funressnfv  27949  ralxfrd2  28049  elfzmlbp  28081  elfz0fzfz0  28088  fz0fzelfz0  28092  elfzonelfzo  28105  hashimarni  28132  swrdnd  28144  swrdvalodmlem1  28149  swrdvalodm2  28150  swrdvalodm  28151  swrd0swrd  28153  swrdswrdlem  28154  swrdswrd  28155  swrdccatin1  28161  swrdccatin12lem3a  28164  swrdccatin2  28166  swrdccatin12lem3  28168  swrdccatin12lem4  28169  swrdccat  28172  swrdccat3blem  28174  2cshw1lem2  28205  2cshwmod  28213  lswrdn0  28216  cshweqdif2s  28224  cshweqrep  28227  cshwssizelem1a  28232  cshwssizelem2  28234  cshwssizelem3  28235  usgra2wlkspthlem2  28250  usgra2pthlem1  28253  el2wlkonot  28279  usg2wotspth  28294  usg2spthonot  28298  usg2spthonot0  28299  usgfiregdegfi  28304  3vfriswmgra  28322  1to2vfriswmgra  28323  1to3vfriswmgra  28324  3cyclfrgrarn  28330  n4cyclfrgra  28335  4cyclusnfrgra  28336  frgranbnb  28337  frgrancvvdeqlemB  28354  frg2wot1  28373  frg2woteqm  28375  frg2woteq  28376  usg2spot2nb  28381  2spotmdisj  28384  usgreghash2spot  28385  frgregordn0  28386  ad5ant13  28474  ad5ant14  28475  ad5ant15  28476  ad5ant134  28486  ad5ant135  28487  ad5ant145  28488  19.41rg  28564  ee223  28662  cbv1hwAUX7  29438  sbiedNEW7  29467  a16gNEW7  29473  sbequiNEW7  29506  cbv1hOLD7  29646  lshpdisj  29712  lub0N  29914  leat2  30019  hlrelat2  30127  cvrexchlem  30143  cvratlem  30145  atcvrj0  30152  cvrat2  30153  snatpsubN  30474  linepsubN  30476  pmaple  30485  pmapsub  30492  elpaddn0  30524  paddasslem5  30548  trlval2  30887  cdlemn11pre  31935  dihord2pre  31950  mapdordlem2  32362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator