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

Theorem 3com23 1157
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 1150 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 72 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
433imp 1145 1  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3coml  1158  syld3an2  1229  3anidm13  1240  eqreu  3033  curry2f  6301  f1ofveu  6426  dfsmo2  6451  nneob  6737  f1oeng  6968  suppr  7309  infdif  7925  axdclem2  8237  gchen1  8337  grumap  8520  grudomon  8529  mul32  9069  add32  9116  subsub23  9146  subadd23  9153  addsub12  9154  subsub  9167  subsub3  9169  sub32  9171  suble  9342  lesub  9343  ltsub23  9344  ltsub13  9345  ltleadd  9347  div32  9534  div13  9535  div12  9536  divdiv32  9558  cju  9832  infmssuzle  10392  ioo0  10773  ico0  10794  ioc0  10795  icc0  10796  fzen  10903  modcyc  11091  expgt0  11228  expge0  11231  expge1  11232  shftval2  11666  abs3dif  11911  divalgb  12700  submrc  13629  mrieqv2d  13640  pltnlt  14201  pltn2lp  14202  lubid  14215  joincomALT  14234  meetcomALT  14236  tosso  14241  latjcom  14264  latmcom  14280  latnle  14290  latabs1  14292  lubel  14325  ipopos  14362  grpinvcnv  14635  mulgneg2  14693  oppgmnd  14926  oddvdsnn0  14958  oddvds  14961  odmulg  14968  odcl2  14977  lsmcomx  15247  rngcom  15468  mulgass2  15486  opprrng  15512  irredrmul  15588  irredlmul  15589  isdrngrd  15637  islmodd  15732  lmodcom  15770  opprdomn  16141  zntoslem  16616  ipcl  16643  rintopn  16761  opnnei  16963  restin  17003  cnpnei  17099  cnprest  17123  ordthaus  17218  kgen2ss  17356  hausflim  17778  fclsfnflim  17824  cnpfcf  17838  opnsubg  17892  xmetsym  18014  ngpdsr  18228  ngpds2r  18230  ngpds3r  18232  clmmulg  18695  iscau2  18807  dgr1term  19745  cxpeq0  20136  cxpge0  20141  grpoidinvlem2  20984  grpoinvdiv  21024  gxcl  21044  nvpncan  21329  nvsub  21347  nvabs  21353  nvelbl  21376  ipval2lem2  21391  ipval2lem5  21397  dipcj  21404  diporthcom  21406  dipdi  21535  dipassr  21538  dipsubdi  21541  hlipcj  21604  hvadd32  21727  hvsub32  21738  his5  21779  hoadd32  22477  hosubsub  22511  unopf1o  22610  adj2  22628  adjvalval  22631  adjlnop  22780  leopmul2i  22829  cvntr  22986  mdsymlem5  23101  sumdmdii  23109  supxrnemnf  23328  unitdivcld  23455  cuspcvg  23591  ghomf1olem  24405  gcd32  24662  cgrrflx  25169  cgrcom  25172  cgrcomr  25179  btwntriv1  25198  cgr3com  25235  colineartriv2  25250  segleantisym  25297  seglelin  25298  btwnoutside  25307  clsint2  25571  heibor1  25857  rngoidl  25972  ispridlc  26018  nerabdioph  26213  monotoddzzfi  26350  fzneg  26392  jm2.19lem2  26406  reccot  27928  bnj605  28701  bnj607  28710  op0le  29445  opltcon3b  29463  cmtcomlemN  29507  cmtcomN  29508  cmt3N  29510  cmtbr3N  29513  cvrval2  29533  cvrnbtwn4  29538  leatb  29551  atl0le  29563  atlrelat1  29580  hlatlej2  29634  hlateq  29657  hlrelat5N  29659  snatpsubN  30008  pmap11  30020  paddcom  30071  sspadd2  30074  paddss12  30077  cdleme51finvN  30814  cdleme51finvtrN  30816  cdlemeiota  30843  cdlemg2jlemOLDN  30851  cdlemg2klem  30853  cdlemg4b1  30867  cdlemg4b2  30868  trljco2  30999  tgrpabl  31009  tendoplcom  31040  cdleml6  31239  erngdvlem3-rN  31256  dia11N  31307  dib11N  31419  dih11  31524
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator