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  2957  curry2f  6214  f1ofveu  6339  dfsmo2  6364  nneob  6650  f1oeng  6880  suppr  7219  infdif  7835  axdclem2  8147  gchen1  8247  grumap  8430  grudomon  8439  mul32  8979  add32  9026  subsub23  9056  subadd23  9063  addsub12  9064  subsub  9077  subsub3  9079  sub32  9081  suble  9252  lesub  9253  ltsub23  9254  ltsub13  9255  ltleadd  9257  div32  9444  div13  9445  div12  9446  divdiv32  9468  cju  9742  infmssuzle  10300  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  fzen  10811  modcyc  10999  expgt0  11135  expge0  11138  expge1  11139  shftval2  11570  abs3dif  11815  divalgb  12603  submrc  13530  mrieqv2d  13541  pltnlt  14102  pltn2lp  14103  lubid  14116  joincomALT  14135  meetcomALT  14137  tosso  14142  latjcom  14165  latmcom  14181  latnle  14191  latabs1  14193  lubel  14226  ipopos  14263  grpinvcnv  14536  mulgneg2  14594  oppgmnd  14827  oddvdsnn0  14859  oddvds  14862  odmulg  14869  odcl2  14878  lsmcomx  15148  rngcom  15369  mulgass2  15387  opprrng  15413  irredrmul  15489  irredlmul  15490  isdrngrd  15538  islmodd  15633  lmodcom  15671  opprdomn  16042  zntoslem  16510  ipcl  16537  rintopn  16655  opnnei  16857  restin  16897  cnpnei  16993  cnprest  17017  ordthaus  17112  kgen2ss  17250  hausflim  17676  fclsfnflim  17722  cnpfcf  17736  opnsubg  17790  xmetsym  17912  ngpdsr  18126  ngpds2r  18128  ngpds3r  18130  clmmulg  18591  iscau2  18703  dgr1term  19641  cxpeq0  20025  cxpge0  20030  grpoidinvlem2  20872  grpoinvdiv  20912  gxcl  20932  nvpncan  21215  nvsub  21233  nvabs  21239  nvelbl  21262  ipval2lem2  21277  ipval2lem5  21283  dipcj  21290  diporthcom  21292  dipdi  21421  dipassr  21424  dipsubdi  21427  hlipcj  21490  hvadd32  21613  hvsub32  21624  his5  21665  hoadd32  22363  hosubsub  22397  unopf1o  22496  adj2  22514  adjvalval  22517  adjlnop  22666  leopmul2i  22715  cvntr  22872  mdsymlem5  22987  sumdmdii  22995  supxrnemnf  23256  unitdivcld  23285  ghomf1olem  24001  gcd32  24104  cgrrflx  24610  cgrcom  24613  cgrcomr  24620  btwntriv1  24639  cgr3com  24676  colineartriv2  24691  segleantisym  24738  seglelin  24739  btwnoutside  24748  elioo1t3  25502  lvsovso2  25627  addcomv  25655  subclcvd  25673  idfisf  25841  clsint2  26247  heibor1  26534  rngoidl  26649  ispridlc  26695  nerabdioph  26890  monotoddzzfi  27027  fzneg  27069  jm2.19lem2  27083  reccot  28228  bnj605  28939  bnj607  28948  op0le  29376  opltcon3b  29394  cmtcomlemN  29438  cmtcomN  29439  cmt3N  29441  cmtbr3N  29444  cvrval2  29464  cvrnbtwn4  29469  leatb  29482  atl0le  29494  atlrelat1  29511  hlatlej2  29565  hlateq  29588  hlrelat5N  29590  snatpsubN  29939  pmap11  29951  paddcom  30002  sspadd2  30005  paddss12  30008  cdleme51finvN  30745  cdleme51finvtrN  30747  cdlemeiota  30774  cdlemg2jlemOLDN  30782  cdlemg2klem  30784  cdlemg4b1  30798  cdlemg4b2  30799  trljco2  30930  tgrpabl  30940  tendoplcom  30971  cdleml6  31170  erngdvlem3-rN  31187  dia11N  31238  dib11N  31350  dih11  31455
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