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

Theorem 3com13 1210
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 993 . 2  |-  ( ( ch  /\  ps  /\  ph )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 198 1  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  3coml  1212  3adant3l  1260  3adant3r  1261  syld3an1  1310  oacan  7257  oaword1  7261  nnacan  7337  nnaword1  7338  elmapg  7493  fisseneq  7789  ltapr  9469  subadd  9877  ltaddsub  10087  leaddsub  10089  iooshf  11713  elfzmlbmOLD  11899  faclbnd4  12479  relexpsucr  13071  relexpsucl  13075  dvdsmulc  14308  lcmdvdsb  14549  infpnlem1  14817  fmf  20891  frgra3v  25575  nvs  26136  dipdi  26329  dipsubdi  26335  spansncol  27056  chirredlem2  27879  mdsymlem3  27893  isbasisrelowllem2  31493  ltflcei  31640  iscringd  31939  iunrelexp0  35936  uun123p4  36842  isosctrlem1ALT  36974  stoweidlem17  37449
  Copyright terms: Public domain W3C validator