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

Theorem 3com12 1192
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 972 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 195 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  3adant2l  1213  3adant2r  1214  brelrng  5169  fresaunres1  5684  fvun2  5864  onfununi  6904  oaword  7090  nnaword  7168  nnmword  7174  ecopovtrn  7305  fpmg  7340  tskord  9050  ltadd2  9581  mul12  9638  add12  9685  addsub  9724  addsubeq4  9728  ppncan  9754  leadd1  9910  ltaddsub2  9917  leaddsub2  9919  ltsub1  9938  ltsub2  9939  div23  10116  ltmul1  10282  ltmulgt11  10292  lediv1  10297  ledivmulOLD  10309  lemuldiv  10314  ltdiv2  10320  zdiv  10815  xltadd1  11322  xltmul1  11358  iooneg  11508  icoshft  11510  fzaddel  11596  fzshftral  11650  facwordi  12168  swrdspsleq  12446  abssubge0  12919  climshftlem  13156  znnenlem  13598  dvdsmul1  13658  divalglem8  13708  divalgb  13712  pcfac  14065  mhmmulg  15763  xrsdsreval  17969  cnmptcom  19369  hmeof1o2  19454  ordthmeo  19493  cxplt2  22261  axcontlem8  23354  vcdi  24067  isvci  24097  dipdi  24380  dipsubdi  24386  hvadd12  24574  hvmulcom  24582  his5  24625  bcs3  24722  chj12  25074  spansnmul  25104  homul12  25346  hoaddsub  25357  lnopmul  25508  lnopaddmuli  25514  lnopsubmuli  25516  lnfnaddmuli  25586  leop2  25665  dmdsl3  25856  chirredlem3  25933  atmd2  25941  cdj3lem3  25979  signstfvc  27111  cnambfre  28580  3com12d  28645  sdclem2  28778  addrcom  29871  stoweidlem17  29952  sigaras  30031  sigarms  30032  clwwlkndivn  30651  3imp21  31579  uun123p1  31844  sineq0ALT  31975
  Copyright terms: Public domain W3C validator