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

Theorem 3com13 1159
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3com13  |-  ( ( ch  /\  ps  /\  ph )  ->  th )

Proof of Theorem 3com13
StepHypRef Expression
1 3anrev 948 . 2  |-  ( ( ch  /\  ps  /\  ph )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 189 1  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  3coml  1161  3adant3l  1181  3adant3r  1182  syld3an1  1231  oacan  6792  oaword1  6796  nnacan  6872  nnaword1  6873  elmapg  7032  fisseneq  7321  ltapr  8923  subadd  9309  ltaddsub  9503  leaddsub  9505  iooshf  10990  faclbnd4  11589  dvdsmulc  12878  infpnlem1  13279  fmf  17978  nvs  22152  dipdi  22345  dipsubdi  22351  spansncol  23071  chirredlem2  23895  mdsymlem3  23909  ltflcei  26240  iscringd  26610  stoweidlem17  27743  elfzmlbm  28107  frgra3v  28393  uun123p4  28925  isosctrlem1ALT  29047
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator