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

Theorem 3com13 1201
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1
Assertion
Ref Expression
3com13

Proof of Theorem 3com13
StepHypRef Expression
1 3anrev 984 . 2
2 3exp.1 . 2
31, 2sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  3coml  1203  3adant3l  1224  3adant3r  1225  syld3an1  1274  oacan  7216  oaword1  7220  nnacan  7296  nnaword1  7297  elmapg  7452  fisseneq  7751  ltapr  9444  subadd  9846  ltaddsub  10051  leaddsub  10053  iooshf  11632  elfzmlbmOLD  11814  faclbnd4  12375  dvdsmulc  14011  infpnlem1  14428  fmf  20446  frgra3v  25002  nvs  25565  dipdi  25758  dipsubdi  25764  spansncol  26486  chirredlem2  27310  mdsymlem3  27324  ltflcei  30043  iscringd  30396  lcmdvdsb  31217  stoweidlem17  31799  uun123p4  33609  isosctrlem1ALT  33734
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
  Copyright terms: Public domain W3C validator