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

Theorem 3com13 1156
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 945 . 2  |-  ( ( ch  /\  ps  /\  ph )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 187 1  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3coml  1158  3adant3l  1178  3adant3r  1179  syld3an1  1228  oacan  6546  oaword1  6550  nnacan  6626  nnaword1  6627  elmapg  6785  fisseneq  7074  ltapr  8669  subadd  9054  ltaddsub  9248  leaddsub  9250  iooshf  10728  faclbnd4  11310  dvdsmulc  12556  infpnlem1  12957  fmf  17640  nvs  21228  dipdi  21421  dipsubdi  21427  spansncol  22147  chirredlem2  22971  mdsymlem3  22985  subaddv  25671  iscringd  26624  stoweidlem17  27766  frgra3v  28180  uun123p4  28587
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator