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  6562  oaword1  6566  nnacan  6642  nnaword1  6643  elmapg  6801  fisseneq  7090  ltapr  8685  subadd  9070  ltaddsub  9264  leaddsub  9266  iooshf  10744  faclbnd4  11326  dvdsmulc  12572  infpnlem1  12973  fmf  17656  nvs  21244  dipdi  21437  dipsubdi  21443  spansncol  22163  chirredlem2  22987  mdsymlem3  23001  ltflcei  24998  subaddv  25774  iscringd  26727  stoweidlem17  27869  frgra3v  28426  uun123p4  28901
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