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

Theorem 3com12 1155
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3com12  |-  ( ( ps  /\  ph  /\  ch )  ->  th )

Proof of Theorem 3com12
StepHypRef Expression
1 3ancoma 941 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 187 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3adant2l  1176  3adant2r  1177  brelrng  4908  fresaunres1  5414  fvun2  5591  onfununi  6358  oaword  6547  nnaword  6625  nnmword  6631  ecopovtrn  6761  fpmg  6793  tskord  8402  ltadd2  8924  mul12  8978  add12  9025  addsub  9062  addsubeq4  9066  ppncan  9089  leadd1  9242  ltaddsub2  9249  leaddsub2  9251  ltsub1  9270  ltsub2  9271  div23  9443  ltmul1  9606  ltmulgt11  9616  lediv1  9621  ledivmulOLD  9630  lemuldiv  9635  ltdiv2  9641  zdiv  10082  xltadd1  10576  xltmul1  10612  iooneg  10756  icoshft  10758  fzaddel  10826  fzshftral  10869  facwordi  11302  abssubge0  11811  climshftlem  12048  znnenlem  12490  dvdsmul1  12550  divalglem8  12599  divalgb  12603  pcfac  12947  mhmmulg  14599  xrsdsreval  16416  cnmptcom  17372  hmeof1o2  17454  ordthmeo  17493  cxplt2  20045  vcdi  21108  isvci  21138  dipdi  21421  dipsubdi  21427  hvadd12  21614  hvmulcom  21622  his5  21665  bcs3  21762  chj12  22113  spansnmul  22143  homul12  22385  hoaddsub  22396  lnopmul  22547  lnopaddmuli  22553  lnopsubmuli  22555  lnfnaddmuli  22625  leop2  22704  dmdsl3  22895  chirredlem3  22972  atmd2  22980  cdj3lem3  23018  axcontlem8  24599  oriso  25214  3com12d  26219  sdclem2  26452  addrcom  27680  stoweidlem17  27766  sigaras  27845  sigarms  27846  3imp21  28334  uun123p1  28584
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