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

Theorem 3com23 1160
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 1153 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 75 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
433imp 1148 1  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  3coml  1161  syld3an2  1232  3anidm13  1243  eqreu  3128  curry2f  6444  f1ofveu  6586  dfsmo2  6611  nneob  6897  f1oeng  7128  suppr  7475  infdif  8091  axdclem2  8402  gchen1  8502  grumap  8685  grudomon  8694  mul32  9235  add32  9282  subsub23  9312  subadd23  9319  addsub12  9320  subsub  9333  subsub3  9335  sub32  9337  suble  9508  lesub  9509  ltsub23  9510  ltsub13  9511  ltleadd  9513  div32  9700  div13  9701  div12  9702  divdiv32  9724  cju  9998  infmssuzle  10560  ioo0  10943  ico0  10964  ioc0  10965  icc0  10966  fzen  11074  modcyc  11278  expgt0  11415  expge0  11418  expge1  11419  shftval2  11892  abs3dif  12137  divalgb  12926  submrc  13855  mrieqv2d  13866  pltnlt  14427  pltn2lp  14428  lubid  14441  joincomALT  14460  meetcomALT  14462  tosso  14467  latjcom  14490  latmcom  14506  latnle  14516  latabs1  14518  lubel  14551  ipopos  14588  grpinvcnv  14861  mulgneg2  14919  oppgmnd  15152  oddvdsnn0  15184  oddvds  15187  odmulg  15194  odcl2  15203  lsmcomx  15473  rngcom  15694  mulgass2  15712  opprrng  15738  irredrmul  15814  irredlmul  15815  isdrngrd  15863  islmodd  15958  lmodcom  15992  opprdomn  16363  zntoslem  16839  ipcl  16866  rintopn  16984  opnnei  17186  restin  17232  cnpnei  17330  cnprest  17355  ordthaus  17450  kgen2ss  17589  hausflim  18015  fclsfnflim  18061  cnpfcf  18075  opnsubg  18139  cuspcvg  18333  psmetsym  18343  xmetsym  18379  ngpdsr  18653  ngpds2r  18655  ngpds3r  18657  clmmulg  19120  iscau2  19232  dgr1term  20180  cxpeq0  20571  cxpge0  20576  grpoidinvlem2  21795  grpoinvdiv  21835  gxcl  21855  nvpncan  22140  nvsub  22158  nvabs  22164  nvelbl  22187  ipval2lem2  22202  ipval2lem5  22208  dipcj  22215  diporthcom  22217  dipdi  22346  dipassr  22349  dipsubdi  22352  hlipcj  22415  hvadd32  22538  hvsub32  22549  his5  22590  hoadd32  23288  hosubsub  23322  unopf1o  23421  adj2  23439  adjvalval  23442  adjlnop  23591  leopmul2i  23640  cvntr  23797  mdsymlem5  23912  sumdmdii  23920  supxrnemnf  24129  tosglb  24194  unitdivcld  24301  ghomf1olem  25107  gcd32  25372  cgrrflx  25923  cgrcom  25926  cgrcomr  25933  btwntriv1  25952  cgr3com  25989  colineartriv2  26004  segleantisym  26051  seglelin  26052  btwnoutside  26061  ftc1anclem5  26286  clsint2  26334  heibor1  26521  rngoidl  26636  ispridlc  26682  nerabdioph  26871  monotoddzzfi  27007  fzneg  27049  jm2.19lem2  27063  elfzmlbm  28108  reccot  28503  sineq0ALT  29051  bnj605  29280  bnj607  29289  op0le  29986  opltcon3b  30004  cmtcomlemN  30048  cmtcomN  30049  cmt3N  30051  cmtbr3N  30054  cvrval2  30074  cvrnbtwn4  30079  leatb  30092  atl0le  30104  atlrelat1  30121  hlatlej2  30175  hlateq  30198  hlrelat5N  30200  snatpsubN  30549  pmap11  30561  paddcom  30612  sspadd2  30615  paddss12  30618  cdleme51finvN  31355  cdleme51finvtrN  31357  cdlemeiota  31384  cdlemg2jlemOLDN  31392  cdlemg2klem  31394  cdlemg4b1  31408  cdlemg4b2  31409  trljco2  31540  tgrpabl  31550  tendoplcom  31581  cdleml6  31780  erngdvlem3-rN  31797  dia11N  31848  dib11N  31960  dih11  32065
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator