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  2970  curry2f  6230  f1ofveu  6355  dfsmo2  6380  nneob  6666  f1oeng  6896  suppr  7235  infdif  7851  axdclem2  8163  gchen1  8263  grumap  8446  grudomon  8455  mul32  8995  add32  9042  subsub23  9072  subadd23  9079  addsub12  9080  subsub  9093  subsub3  9095  sub32  9097  suble  9268  lesub  9269  ltsub23  9270  ltsub13  9271  ltleadd  9273  div32  9460  div13  9461  div12  9462  divdiv32  9484  cju  9758  infmssuzle  10316  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  fzen  10827  modcyc  11015  expgt0  11151  expge0  11154  expge1  11155  shftval2  11586  abs3dif  11831  divalgb  12619  submrc  13546  mrieqv2d  13557  pltnlt  14118  pltn2lp  14119  lubid  14132  joincomALT  14151  meetcomALT  14153  tosso  14158  latjcom  14181  latmcom  14197  latnle  14207  latabs1  14209  lubel  14242  ipopos  14279  grpinvcnv  14552  mulgneg2  14610  oppgmnd  14843  oddvdsnn0  14875  oddvds  14878  odmulg  14885  odcl2  14894  lsmcomx  15164  rngcom  15385  mulgass2  15403  opprrng  15429  irredrmul  15505  irredlmul  15506  isdrngrd  15554  islmodd  15649  lmodcom  15687  opprdomn  16058  zntoslem  16526  ipcl  16553  rintopn  16671  opnnei  16873  restin  16913  cnpnei  17009  cnprest  17033  ordthaus  17128  kgen2ss  17266  hausflim  17692  fclsfnflim  17738  cnpfcf  17752  opnsubg  17806  xmetsym  17928  ngpdsr  18142  ngpds2r  18144  ngpds3r  18146  clmmulg  18607  iscau2  18719  dgr1term  19657  cxpeq0  20041  cxpge0  20046  grpoidinvlem2  20888  grpoinvdiv  20928  gxcl  20948  nvpncan  21231  nvsub  21249  nvabs  21255  nvelbl  21278  ipval2lem2  21293  ipval2lem5  21299  dipcj  21306  diporthcom  21308  dipdi  21437  dipassr  21440  dipsubdi  21443  hlipcj  21506  hvadd32  21629  hvsub32  21640  his5  21681  hoadd32  22379  hosubsub  22413  unopf1o  22512  adj2  22530  adjvalval  22533  adjlnop  22682  leopmul2i  22731  cvntr  22888  mdsymlem5  23003  sumdmdii  23011  supxrnemnf  23271  unitdivcld  23300  ghomf1olem  24016  gcd32  24175  cgrrflx  24682  cgrcom  24685  cgrcomr  24692  btwntriv1  24711  cgr3com  24748  colineartriv2  24763  segleantisym  24810  seglelin  24811  btwnoutside  24820  elioo1t3  25605  lvsovso2  25730  addcomv  25758  subclcvd  25776  idfisf  25944  clsint2  26350  heibor1  26637  rngoidl  26752  ispridlc  26798  nerabdioph  26993  monotoddzzfi  27130  fzneg  27172  jm2.19lem2  27186  reccot  28482  bnj605  29255  bnj607  29264  op0le  29998  opltcon3b  30016  cmtcomlemN  30060  cmtcomN  30061  cmt3N  30063  cmtbr3N  30066  cvrval2  30086  cvrnbtwn4  30091  leatb  30104  atl0le  30116  atlrelat1  30133  hlatlej2  30187  hlateq  30210  hlrelat5N  30212  snatpsubN  30561  pmap11  30573  paddcom  30624  sspadd2  30627  paddss12  30630  cdleme51finvN  31367  cdleme51finvtrN  31369  cdlemeiota  31396  cdlemg2jlemOLDN  31404  cdlemg2klem  31406  cdlemg4b1  31420  cdlemg4b2  31421  trljco2  31552  tgrpabl  31562  tendoplcom  31593  cdleml6  31792  erngdvlem3-rN  31809  dia11N  31860  dib11N  31972  dih11  32077
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