Theorem ud1lem0ab 257

Description: Join both sides of hypotheses with →₁ . (Contributed by NM, 19-Dec-1998.)

Hypotheses

Ref	Expression
ud1lem0ab.1	a = b
ud1lem0ab.2	c = d

Assertion

Ref	Expression
ud1lem0ab	(a →1 c) = (b →1 d)

Proof of Theorem ud1lem0ab

Step	Hyp	Ref	Expression
1		ud1lem0ab.1	. . 3 a = b
2	1	ud1lem0b 256	. 2 (a →1 c) = (b →1 c)
3		ud1lem0ab.2	. . 3 c = d
4	3	ud1lem0a 255	. 2 (b →1 c) = (b →1 d)
5	2, 4	ax-r2 36	1 (a →1 c) = (b →1 d)

Syntax hints:   = wb 1   →₁ wi1 12

This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-i1 44

This theorem is referenced by:  1oai1  821  gomaex3  924  oa3to4lem6  950  oa4to6  965