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

Theorem 3com13 1201
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 984 . 2  |-  ( ( ch  /\  ps  /\  ph )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 195 1  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  3coml  1203  3adant3l  1224  3adant3r  1225  syld3an1  1274  oacan  7198  oaword1  7202  nnacan  7278  nnaword1  7279  elmapg  7434  fisseneq  7732  ltapr  9424  subadd  9824  ltaddsub  10027  leaddsub  10029  iooshf  11604  elfzmlbm  11783  faclbnd4  12344  dvdsmulc  13875  infpnlem1  14290  fmf  20273  frgra3v  24775  nvs  25338  dipdi  25531  dipsubdi  25537  spansncol  26259  chirredlem2  27083  mdsymlem3  27097  ltflcei  29896  iscringd  30226  lcmdvdsb  31044  stoweidlem17  31544  uun123p4  32906  isosctrlem1ALT  33031
  Copyright terms: Public domain W3C validator