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

Theorem 3com12 1157
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 943 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 188 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  3adant2l  1178  3adant2r  1179  brelrng  5085  fresaunres1  5602  fvun2  5781  onfununi  6589  oaword  6778  nnaword  6856  nnmword  6862  ecopovtrn  6993  fpmg  7025  tskord  8639  ltadd2  9161  mul12  9216  add12  9263  addsub  9300  addsubeq4  9304  ppncan  9327  leadd1  9480  ltaddsub2  9487  leaddsub2  9489  ltsub1  9508  ltsub2  9509  div23  9681  ltmul1  9844  ltmulgt11  9854  lediv1  9859  ledivmulOLD  9868  lemuldiv  9873  ltdiv2  9879  zdiv  10324  xltadd1  10819  xltmul1  10855  iooneg  11001  icoshft  11003  fzaddel  11071  fzshftral  11117  facwordi  11563  abssubge0  12114  climshftlem  12351  znnenlem  12794  dvdsmul1  12854  divalglem8  12903  divalgb  12907  pcfac  13251  mhmmulg  14905  xrsdsreval  16726  cnmptcom  17693  hmeof1o2  17778  ordthmeo  17817  cxplt2  20572  vcdi  22014  isvci  22044  dipdi  22327  dipsubdi  22333  hvadd12  22520  hvmulcom  22528  his5  22571  bcs3  22668  chj12  23019  spansnmul  23049  homul12  23291  hoaddsub  23302  lnopmul  23453  lnopaddmuli  23459  lnopsubmuli  23461  lnfnaddmuli  23531  leop2  23610  dmdsl3  23801  chirredlem3  23878  atmd2  23886  cdj3lem3  23924  axcontlem8  25853  cnambfre  26196  3com12d  26245  sdclem2  26378  addrcom  27589  stoweidlem17  27675  sigaras  27754  sigarms  27755  3imp21  28408  uun123p1  28673
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator