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  3135  curry2f  6478  f1ofveu  6620  dfsmo2  6645  nneob  6931  f1oeng  7162  suppr  7509  infdif  8127  axdclem2  8438  gchen1  8538  grumap  8721  grudomon  8730  mul32  9271  add32  9318  subsub23  9348  subadd23  9355  addsub12  9356  subsub  9369  subsub3  9371  sub32  9373  suble  9544  lesub  9545  ltsub23  9546  ltsub13  9547  ltleadd  9549  div32  9736  div13  9737  div12  9738  divdiv32  9760  cju  10034  infmssuzle  10596  ioo0  10979  ico0  11000  ioc0  11001  icc0  11002  fzen  11110  modcyc  11314  expgt0  11451  expge0  11454  expge1  11455  shftval2  11928  abs3dif  12173  divalgb  12962  submrc  13891  mrieqv2d  13902  pltnlt  14463  pltn2lp  14464  lubid  14477  joincomALT  14496  meetcomALT  14498  tosso  14503  latjcom  14526  latmcom  14542  latnle  14552  latabs1  14554  lubel  14587  ipopos  14624  grpinvcnv  14897  mulgneg2  14955  oppgmnd  15188  oddvdsnn0  15220  oddvds  15223  odmulg  15230  odcl2  15239  lsmcomx  15509  rngcom  15730  mulgass2  15748  opprrng  15774  irredrmul  15850  irredlmul  15851  isdrngrd  15899  islmodd  15994  lmodcom  16028  opprdomn  16399  zntoslem  16875  ipcl  16902  rintopn  17020  opnnei  17222  restin  17268  cnpnei  17366  cnprest  17391  ordthaus  17486  kgen2ss  17625  hausflim  18051  fclsfnflim  18097  cnpfcf  18111  opnsubg  18175  cuspcvg  18369  psmetsym  18379  xmetsym  18415  ngpdsr  18689  ngpds2r  18691  ngpds3r  18693  clmmulg  19156  iscau2  19268  dgr1term  20216  cxpeq0  20607  cxpge0  20612  grpoidinvlem2  21831  grpoinvdiv  21871  gxcl  21891  nvpncan  22176  nvsub  22194  nvabs  22200  nvelbl  22223  ipval2lem2  22238  ipval2lem5  22244  dipcj  22251  diporthcom  22253  dipdi  22382  dipassr  22385  dipsubdi  22388  hlipcj  22451  hvadd32  22574  hvsub32  22585  his5  22626  hoadd32  23324  hosubsub  23358  unopf1o  23457  adj2  23475  adjvalval  23478  adjlnop  23627  leopmul2i  23676  cvntr  23833  mdsymlem5  23948  sumdmdii  23956  supxrnemnf  24162  tosglb  24227  unitdivcld  24334  ghomf1olem  25140  gcd32  25405  cgrrflx  25956  cgrcom  25959  cgrcomr  25966  btwntriv1  25985  cgr3com  26022  colineartriv2  26037  segleantisym  26084  seglelin  26085  btwnoutside  26094  ftc1anclem5  26326  clsint2  26374  heibor1  26561  rngoidl  26676  ispridlc  26722  nerabdioph  26981  monotoddzzfi  27117  fzneg  27159  jm2.19lem2  27173  elfzmlbm  28227  reccot  28673  sineq0ALT  29223  bnj605  29452  bnj607  29461  op0le  30158  opltcon3b  30176  cmtcomlemN  30220  cmtcomN  30221  cmt3N  30223  cmtbr3N  30226  cvrval2  30246  cvrnbtwn4  30251  leatb  30264  atl0le  30276  atlrelat1  30293  hlatlej2  30347  hlateq  30370  hlrelat5N  30372  snatpsubN  30721  pmap11  30733  paddcom  30784  sspadd2  30787  paddss12  30790  cdleme51finvN  31527  cdleme51finvtrN  31529  cdlemeiota  31556  cdlemg2jlemOLDN  31564  cdlemg2klem  31566  cdlemg4b1  31580  cdlemg4b2  31581  trljco2  31712  tgrpabl  31722  tendoplcom  31753  cdleml6  31952  erngdvlem3-rN  31969  dia11N  32020  dib11N  32132  dih11  32237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator