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

Theorem 3com12 1195
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 975 . 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 968
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 970
This theorem is referenced by:  3adant2l  1217  3adant2r  1218  brelrng  5225  fresaunres1  5751  fvun2  5932  onfununi  7004  oaword  7190  nnaword  7268  nnmword  7274  ecopovtrn  7406  fpmg  7436  tskord  9149  ltadd2  9679  mul12  9736  add12  9783  addsub  9822  addsubeq4  9826  ppncan  9852  leadd1  10011  ltaddsub2  10018  leaddsub2  10020  ltsub1  10039  ltsub2  10040  div23  10217  ltmul1  10383  ltmulgt11  10393  lediv1  10398  ledivmulOLD  10410  lemuldiv  10415  ltdiv2  10421  zdiv  10922  xltadd1  11439  xltmul1  11475  iooneg  11631  icoshft  11633  fzaddel  11709  fzshftral  11756  facwordi  12324  swrdspsleq  12625  abssubge0  13111  climshftlem  13348  znnenlem  13797  dvdsmul1  13857  divalglem8  13908  divalgb  13912  pcfac  14268  mhmmulg  15969  xrsdsreval  18226  cnmptcom  19909  hmeof1o2  19994  ordthmeo  20033  cxplt2  22802  axcontlem8  23945  clwwlkndivn  24501  vcdi  25109  isvci  25139  dipdi  25422  dipsubdi  25428  hvadd12  25616  hvmulcom  25624  his5  25667  bcs3  25764  chj12  26116  spansnmul  26146  homul12  26388  hoaddsub  26399  lnopmul  26550  lnopaddmuli  26556  lnopsubmuli  26558  lnfnaddmuli  26628  leop2  26707  dmdsl3  26898  chirredlem3  26975  atmd2  26983  cdj3lem3  27021  signstfvc  28159  cnambfre  29629  3com12d  29694  sdclem2  29827  addrcom  30919  stoweidlem17  31274  sigaras  31496  sigarms  31497  3imp21  32298  uun123p1  32563  sineq0ALT  32694
  Copyright terms: Public domain W3C validator