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

Theorem 3com12 1200
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 980 . 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 973
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 975
This theorem is referenced by:  3adant2l  1222  3adant2r  1223  brelrng  5242  fresaunres1  5764  fvun2  5945  onfununi  7030  oaword  7216  nnaword  7294  nnmword  7300  ecopovtrn  7432  fpmg  7463  tskord  9175  ltadd2  9705  mul12  9763  add12  9810  addsub  9850  addsubeq4  9854  ppncan  9880  leadd1  10041  ltaddsub2  10048  leaddsub2  10050  ltsub1  10069  ltsub2  10070  div23  10247  ltmul1  10413  ltmulgt11  10423  lediv1  10428  lemuldiv  10444  ltdiv2  10450  zdiv  10954  xltadd1  11473  xltmul1  11509  iooneg  11665  icoshft  11667  fzaddel  11743  fzshftral  11791  facwordi  12369  abssubge0  13171  climshftlem  13408  znnenlem  13956  dvdsmul1  14016  divalglem8  14069  divalgb  14073  pcfac  14429  mhmmulg  16300  xrsdsreval  18589  cnmptcom  20304  hmeof1o2  20389  ordthmeo  20428  cxplt2  23204  axcontlem8  24400  clwwlkndivn  24963  vcdi  25571  isvci  25601  dipdi  25884  dipsubdi  25890  hvadd12  26078  hvmulcom  26086  his5  26129  bcs3  26226  chj12  26578  spansnmul  26608  homul12  26850  hoaddsub  26861  lnopmul  27012  lnopaddmuli  27018  lnopsubmuli  27020  lnfnaddmuli  27090  leop2  27169  dmdsl3  27360  chirredlem3  27437  atmd2  27445  cdj3lem3  27483  signstfvc  28706  cnambfre  30225  3com12d  30290  sdclem2  30397  lcmgcdeq  31378  addrcom  31546  stoweidlem17  31960  sigaras  32233  sigarms  32234  3imp21  33442  uun123p1  33707  sineq0ALT  33838
  Copyright terms: Public domain W3C validator