Theorem sbequ1 1991

Description: An equality theorem for substitution. (Contributed by NM, 16-May-1993.)

Assertion

Ref	Expression
sbequ1

Proof of Theorem sbequ1

Step	Hyp	Ref	Expression
1		pm3.4 561	. . 3
2		19.8a 1857	. . 3
3		df-sb 1740	. . 3
4	1, 2, 3	sylanbrc 664	. 2
5	4	ex 434	1

Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  [wsb 1739

This theorem is referenced by:  sbequ12  1992  dfsb2  2114  sbequi  2116  sbi1  2133  2eu6  2383  sb5ALT  33295  2pm13.193  33325  2pm13.193VD  33703  sb5ALTVD  33713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-sb 1740