MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com23 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  1378  a16gOLD  2013  cbv1h  2031  sbied  2085  sbequi  2108  ax11indn  2245  eqrdav  2403  ralrimdva  2756  ralrimdvva  2761  ceqsalt  2938  vtoclgft  2962  reu6  3083  sbciegft  3151  reuss2  3581  reupick  3585  pwssun  4449  wefrc  4536  tz7.7  4567  ordtr2  4585  onmindif  4630  unizlim  4657  reusv2lem3  4685  reusv3  4690  limsssuc  4789  tfindsg  4799  limomss  4809  findsg  4831  ssrel  4923  ssrel2  4925  ssrelrel  4935  funssres  5452  funcnvuni  5477  fv3  5703  fvmptt  5779  funfvima2  5933  isoini  6017  isopolem  6024  f1oweALT  6033  weniso  6034  f1ocnv2d  6254  bropopvvv  6385  f1o2ndf1  6413  frxp  6415  riotasv2dOLD  6554  riotasv3dOLD  6558  onfununi  6562  tfrlem1  6595  tz7.49  6661  omordi  6768  omlimcl  6780  omass  6782  oeordsuc  6796  nnmordi  6833  nnmord  6834  omabs  6849  xpdom2  7162  infensuc  7244  findcard2  7307  findcard3  7309  frfi  7311  xpfi  7337  dffi2  7386  elfiun  7393  ordiso2  7440  ordtypelem7  7449  suc11reg  7530  inf3lem2  7540  noinfep  7570  noinfepOLD  7571  cantnfle  7582  cantnflem1  7601  cantnf  7605  trcl  7620  epfrs  7623  r1sdom  7656  pr2ne  7845  dfac8alem  7866  indcardi  7878  alephordi  7911  dfac12lem3  7981  pwsdompw  8040  cofsmo  8105  cfcoflem  8108  coftr  8109  isf32lem2  8190  isf32lem9  8197  axcc3  8274  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  zorn2lem4  8335  zorn2lem6  8337  zorn2lem7  8338  ttukeylem6  8350  uniimadom  8375  konigthlem  8399  fpwwe2lem8  8468  tskord  8611  tskcard  8612  grupr  8628  gruiin  8641  grudomon  8648  grur1a  8650  nqereu  8762  genpn0  8836  genpcd  8839  distrlem5pr  8860  psslinpr  8864  ltaddpr  8867  ltexprlem3  8871  ltexprlem6  8874  ltapr  8878  prlem936  8880  suplem1pr  8885  axpre-sup  9000  1re  9046  ltletr  9122  lemul12a  9824  divgt0  9834  divge0  9835  lbreu  9914  sup2  9920  infmrcl  9943  bndndx  10176  elnnz  10248  uzindOLD  10320  fzind  10324  fnn0ind  10325  uzwo  10495  uzwoOLD  10496  eqreznegel  10517  lbzbi  10520  zmax  10527  zbtwnre  10528  irradd  10554  irrmul  10555  xrltletr  10703  xrub  10846  supxrunb2  10855  iccid  10917  fzm1  11082  fzrevral  11086  elfznelfzo  11147  elfznelfzob  11148  injresinjlem  11154  uzindi  11275  le2sq2  11412  sqlecan  11442  facdiv  11533  facwordi  11535  faclbnd  11536  hashle00  11624  brfi1uzind  11670  ccatopth2  11732  cau3lem  12113  caubnd  12117  climrlim2  12296  rlimuni  12299  rlimcn2  12339  mulcn2  12344  rlimno1  12402  climcau  12419  climbdd  12420  caucvg  12427  xpnnenOLD  12764  dvdsle  12850  ndvdssub  12882  gcdcllem1  12966  dvdslegcd  12971  bezoutlem4  12996  coprmdvds  13057  coprmdvds2  13058  prmfac1  13073  pcqcl  13185  prmpwdvds  13227  infpnlem1  13233  joinle  14405  meetle  14412  clatleglb  14508  sylow2blem3  15211  lsmdisj2  15269  frgpnabllem1  15439  dprddisj2  15552  lssssr  15984  lss1d  15994  lspsncv0  16173  znrrg  16801  uniopn  16925  opnnei  17139  neindisj2  17142  restcls  17199  restntr  17200  tgcnp  17271  subbascn  17272  iscnp4  17281  lmcnp  17322  lpcls  17382  cmpsublem  17416  cmpsub  17417  tgcmp  17418  cmpcld  17419  dfcon2  17435  1stcrest  17469  2ndcdisj  17472  1stccnp  17478  kgencn2  17542  txlm  17633  kqreglem1  17726  filin  17839  isfil2  17841  fgss2  17859  fgfil  17860  ufilmax  17892  ufileu  17904  filufint  17905  cfinufil  17913  elfm2  17933  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  flimopn  17960  fbflim2  17962  flffbas  17980  fclsnei  18004  flimfnfcls  18013  fclscmp  18015  ufilcmp  18017  fcfnei  18020  cnpfcf  18026  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem4  18039  divstgplem  18103  tsmsres  18126  tsmsxp  18137  metss  18491  metcnp3  18523  ivthlem2  19302  ivthlem3  19303  ovoliunnul  19356  ovolicc2lem3  19368  dyadmax  19443  itg2le  19584  itgcn  19687  ellimc3  19719  lhop1  19851  dvfsumrlim  19868  fta1g  20043  fta1  20178  aalioulem3  20204  aalioulem4  20205  ulmcaulem  20263  ulmcau  20264  xrlimcnp  20760  cxploglim  20769  jensen  20780  lgsquad2lem2  21096  2sqlem6  21106  usgranloopv  21351  usgranloop  21352  usgra2edg  21355  usgraedg4  21359  usgra1v  21362  usgraidx2vlem2  21364  usgrafisindb0  21375  usgrafisindb1  21376  usgrares1  21377  cusgrarn  21421  cusgrares  21434  cusgrasize2inds  21439  cusgrafi  21444  sizeusglecusg  21448  usgrnloop  21516  1pthoncl  21545  wlkdvspthlem  21560  wlkdvspth  21561  cyclnspth  21571  fargshiftfo  21578  fargshiftfva  21579  usgrcyclnl1  21580  nvnencycllem  21583  constr3trllem2  21591  4cycl4dv  21607  eupatrl  21643  rngoueqz  21971  nmoub3i  22227  ipasslem5  22289  htthlem  22373  ocin  22751  spansneleq  23025  spansnss  23026  elspansn4  23028  h1datomi  23036  nmopub2tALT  23365  nmfnleub2  23382  hstel2  23675  cvnbtwn  23742  spansncv2  23749  dmdmd  23756  dmdbr3  23761  dmdbr4  23762  dmdbr5  23764  mdsl0  23766  mdexchi  23791  cvexchlem  23824  atcv1  23836  atomli  23838  atcvatlem  23841  atcvat2i  23843  chirredi  23850  mdsymlem3  23861  mdsymlem4  23862  sumdmdii  23871  sumdmdlem  23874  cdj1i  23889  f1o3d  23994  cvxpcon  24882  ghomf1olem  25058  dedekindle  25141  fundmpss  25336  dfon2lem6  25358  dfon2lem8  25360  dfon2lem9  25361  dfon2  25362  predpo  25398  trpredrec  25455  soseq  25468  wfr3g  25469  wfrlem12  25481  frr3g  25494  frrlem11  25507  nodenselem5  25553  nodenselem7  25555  nodenselem8  25556  nofulllem5  25574  brbtwn2  25748  ax5seglem5  25776  axcontlem4  25810  axcontlem10  25816  colinearxfr  25913  btwnconn1lem11  25935  lineintmo  25995  ordcmp  26101  ee7.2aOLD  26115  bddiblnc  26174  trer  26209  elicc3  26210  finminlem  26211  nn0prpwlem  26215  fnessref  26263  comppfsc  26277  neibastop2  26280  fgmin  26289  tailfb  26296  fdc  26339  heibor1lem  26408  ghomco  26448  unichnidl  26531  dmncan1  26576  pell1qrgap  26827  dford3lem1  26987  hbtlem5  27200  symggen  27279  psgnunilem4  27288  sbiota1  27502  funressnfv  27859  elfzmlbp  27978  elfzonelfzo  27992  hashimarni  27995  swrdnd  28001  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin12lem3a  28021  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12  28026  swrdccatin12b  28027  swrdccat3  28029  swrdccat3b  28031  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  el2wlkonot  28066  usg2wotspth  28081  usg2spthonot  28085  usg2spthonot0  28086  usgfiregdegfi  28091  3vfriswmgra  28109  1to2vfriswmgra  28110  1to3vfriswmgra  28111  3cyclfrgrarn  28117  n4cyclfrgra  28122  4cyclusnfrgra  28123  frgranbnb  28124  frgrancvvdeqlemB  28141  frg2wot1  28160  frg2woteqm  28162  frg2woteq  28163  usg2spot2nb  28168  2spotmdisj  28171  usgreghash2spot  28172  frgregordn0  28173  ad5ant13  28261  ad5ant14  28262  ad5ant15  28263  ad5ant134  28273  ad5ant135  28274  ad5ant145  28275  19.41rg  28348  ee223  28444  cbv1hwAUX7  29217  sbiedNEW7  29244  a16gNEW7  29250  sbequiNEW7  29282  cbv1hOLD7  29403  lshpdisj  29470  lub0N  29672  leat2  29777  hlrelat2  29885  cvrexchlem  29901  cvratlem  29903  atcvrj0  29910  cvrat2  29911  snatpsubN  30232  linepsubN  30234  pmaple  30243  pmapsub  30250  elpaddn0  30282  paddasslem5  30306  trlval2  30645  cdlemn11pre  31693  dihord2pre  31708  mapdordlem2  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator