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

Theorem 3com23 1159
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3com23  |-  ( (
ph  /\  ch  /\  ps )  ->  th )

Proof of Theorem 3com23
StepHypRef Expression
1 3exp.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1152 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 74 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
433imp 1147 1  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  3coml  1160  syld3an2  1231  3anidm13  1242  eqreu  3090  curry2f  6405  f1ofveu  6547  dfsmo2  6572  nneob  6858  f1oeng  7089  suppr  7433  infdif  8049  axdclem2  8360  gchen1  8460  grumap  8643  grudomon  8652  mul32  9193  add32  9240  subsub23  9270  subadd23  9277  addsub12  9278  subsub  9291  subsub3  9293  sub32  9295  suble  9466  lesub  9467  ltsub23  9468  ltsub13  9469  ltleadd  9471  div32  9658  div13  9659  div12  9660  divdiv32  9682  cju  9956  infmssuzle  10518  ioo0  10901  ico0  10922  ioc0  10923  icc0  10924  fzen  11032  modcyc  11235  expgt0  11372  expge0  11375  expge1  11376  shftval2  11849  abs3dif  12094  divalgb  12883  submrc  13812  mrieqv2d  13823  pltnlt  14384  pltn2lp  14385  lubid  14398  joincomALT  14417  meetcomALT  14419  tosso  14424  latjcom  14447  latmcom  14463  latnle  14473  latabs1  14475  lubel  14508  ipopos  14545  grpinvcnv  14818  mulgneg2  14876  oppgmnd  15109  oddvdsnn0  15141  oddvds  15144  odmulg  15151  odcl2  15160  lsmcomx  15430  rngcom  15651  mulgass2  15669  opprrng  15695  irredrmul  15771  irredlmul  15772  isdrngrd  15820  islmodd  15915  lmodcom  15949  opprdomn  16320  zntoslem  16796  ipcl  16823  rintopn  16941  opnnei  17143  restin  17188  cnpnei  17286  cnprest  17311  ordthaus  17406  kgen2ss  17544  hausflim  17970  fclsfnflim  18016  cnpfcf  18030  opnsubg  18094  cuspcvg  18288  psmetsym  18298  xmetsym  18334  ngpdsr  18608  ngpds2r  18610  ngpds3r  18612  clmmulg  19075  iscau2  19187  dgr1term  20135  cxpeq0  20526  cxpge0  20531  grpoidinvlem2  21750  grpoinvdiv  21790  gxcl  21810  nvpncan  22095  nvsub  22113  nvabs  22119  nvelbl  22142  ipval2lem2  22157  ipval2lem5  22163  dipcj  22170  diporthcom  22172  dipdi  22301  dipassr  22304  dipsubdi  22307  hlipcj  22370  hvadd32  22493  hvsub32  22504  his5  22545  hoadd32  23243  hosubsub  23277  unopf1o  23376  adj2  23394  adjvalval  23397  adjlnop  23546  leopmul2i  23595  cvntr  23752  mdsymlem5  23867  sumdmdii  23875  supxrnemnf  24084  tosglb  24149  unitdivcld  24256  ghomf1olem  25062  gcd32  25322  cgrrflx  25829  cgrcom  25832  cgrcomr  25839  btwntriv1  25858  cgr3com  25895  colineartriv2  25910  segleantisym  25957  seglelin  25958  btwnoutside  25967  clsint2  26226  heibor1  26413  rngoidl  26528  ispridlc  26574  nerabdioph  26763  monotoddzzfi  26899  fzneg  26941  jm2.19lem2  26955  elfzmlbm  27981  reccot  28219  bnj605  28988  bnj607  28997  op0le  29673  opltcon3b  29691  cmtcomlemN  29735  cmtcomN  29736  cmt3N  29738  cmtbr3N  29741  cvrval2  29761  cvrnbtwn4  29766  leatb  29779  atl0le  29791  atlrelat1  29808  hlatlej2  29862  hlateq  29885  hlrelat5N  29887  snatpsubN  30236  pmap11  30248  paddcom  30299  sspadd2  30302  paddss12  30305  cdleme51finvN  31042  cdleme51finvtrN  31044  cdlemeiota  31071  cdlemg2jlemOLDN  31079  cdlemg2klem  31081  cdlemg4b1  31095  cdlemg4b2  31096  trljco2  31227  tgrpabl  31237  tendoplcom  31268  cdleml6  31467  erngdvlem3-rN  31484  dia11N  31535  dib11N  31647  dih11  31752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator