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

Theorem 3com12 1209
Description: Commutation in antecedent. Swap 1st and 2nd. (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 989 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 198 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  3adant2l  1258  3adant2r  1259  brelrng  5075  fresaunres1  5764  fvun2  5944  onfununi  7059  oaword  7249  nnaword  7327  nnmword  7333  ecopovtrn  7465  fpmg  7496  tskord  9194  ltadd2  9727  mul12  9788  add12  9835  addsub  9875  addsubeq4  9879  ppncan  9905  leadd1  10071  ltaddsub2  10078  leaddsub2  10080  ltsub1  10099  ltsub2  10100  div23  10278  ltmul1  10444  ltmulgt11  10454  lediv1  10459  lemuldiv  10475  ltdiv2  10481  zdiv  10995  xltadd1  11531  xltmul1  11567  iooneg  11739  icoshft  11741  fzaddel  11820  fzshftral  11869  facwordi  12460  abssubge0  13358  climshftlem  13605  znnenlem  14231  dvdsmul1  14291  divalglem8  14345  divalgb  14349  lcmgcdeq  14537  pcfac  14796  mhmmulg  16734  xrsdsreval  18941  cnmptcom  20617  hmeof1o2  20702  ordthmeo  20741  cxplt2  23505  axcontlem8  24844  clwwlkndivn  25407  vcdi  26013  isvci  26043  dipdi  26326  dipsubdi  26332  hvadd12  26520  hvmulcom  26528  his5  26571  bcs3  26668  chj12  27019  spansnmul  27049  homul12  27290  hoaddsub  27301  lnopmul  27452  lnopaddmuli  27458  lnopsubmuli  27460  lnfnaddmuli  27530  leop2  27609  dmdsl3  27800  chirredlem3  27877  atmd2  27885  cdj3lem3  27923  signstfvc  29248  3com12d  30748  cnambfre  31693  sdclem2  31775  addrcom  36469  3imp21  36576  uun123p1  36840  sineq0ALT  36978  stoweidlem17  37450  sigaras  37868  sigarms  37869
  Copyright terms: Public domain W3C validator