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  4924  fresaunres1  5430  fvun2  5607  onfununi  6374  oaword  6563  nnaword  6641  nnmword  6647  ecopovtrn  6777  fpmg  6809  tskord  8418  ltadd2  8940  mul12  8994  add12  9041  addsub  9078  addsubeq4  9082  ppncan  9105  leadd1  9258  ltaddsub2  9265  leaddsub2  9267  ltsub1  9286  ltsub2  9287  div23  9459  ltmul1  9622  ltmulgt11  9632  lediv1  9637  ledivmulOLD  9646  lemuldiv  9651  ltdiv2  9657  zdiv  10098  xltadd1  10592  xltmul1  10628  iooneg  10772  icoshft  10774  fzaddel  10842  fzshftral  10885  facwordi  11318  abssubge0  11827  climshftlem  12064  znnenlem  12506  dvdsmul1  12566  divalglem8  12615  divalgb  12619  pcfac  12963  mhmmulg  14615  xrsdsreval  16432  cnmptcom  17388  hmeof1o2  17470  ordthmeo  17509  cxplt2  20061  vcdi  21124  isvci  21154  dipdi  21437  dipsubdi  21443  hvadd12  21630  hvmulcom  21638  his5  21681  bcs3  21778  chj12  22129  spansnmul  22159  homul12  22401  hoaddsub  22412  lnopmul  22563  lnopaddmuli  22569  lnopsubmuli  22571  lnfnaddmuli  22641  leop2  22720  dmdsl3  22911  chirredlem3  22988  atmd2  22996  cdj3lem3  23034  axcontlem8  24671  oriso  25317  3com12d  26322  sdclem2  26555  addrcom  27783  stoweidlem17  27869  sigaras  27948  sigarms  27949  3imp21  28633  uun123p1  28898
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