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

Step	Hyp	Ref	Expression
1		3anrev 984	. 2
2		3exp.1	. 2
3	1, 2	sylbi 195	1

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