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

Theorem 3com12 1158
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 944 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 189 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  3adant2l  1179  3adant2r  1180  brelrng  5102  fresaunres1  5619  fvun2  5798  onfununi  6606  oaword  6795  nnaword  6873  nnmword  6879  ecopovtrn  7010  fpmg  7042  tskord  8660  ltadd2  9182  mul12  9237  add12  9284  addsub  9321  addsubeq4  9325  ppncan  9348  leadd1  9501  ltaddsub2  9508  leaddsub2  9510  ltsub1  9529  ltsub2  9530  div23  9702  ltmul1  9865  ltmulgt11  9875  lediv1  9880  ledivmulOLD  9889  lemuldiv  9894  ltdiv2  9900  zdiv  10345  xltadd1  10840  xltmul1  10876  iooneg  11022  icoshft  11024  fzaddel  11092  fzshftral  11139  facwordi  11585  abssubge0  12136  climshftlem  12373  znnenlem  12816  dvdsmul1  12876  divalglem8  12925  divalgb  12929  pcfac  13273  mhmmulg  14927  xrsdsreval  16748  cnmptcom  17715  hmeof1o2  17800  ordthmeo  17839  cxplt2  20594  vcdi  22036  isvci  22066  dipdi  22349  dipsubdi  22355  hvadd12  22542  hvmulcom  22550  his5  22593  bcs3  22690  chj12  23041  spansnmul  23071  homul12  23313  hoaddsub  23324  lnopmul  23475  lnopaddmuli  23481  lnopsubmuli  23483  lnfnaddmuli  23553  leop2  23632  dmdsl3  23823  chirredlem3  23900  atmd2  23908  cdj3lem3  23946  axcontlem8  25915  cnambfre  26267  3com12d  26327  sdclem2  26460  addrcom  27670  stoweidlem17  27756  sigaras  27835  sigarms  27836  3imp21  28729  uun123p1  28995  sineq0ALT  29123
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator