Theorem lem3.3.7i0e3 1058

Description: Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the third part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Assertion

Ref	Expression
lem3.3.7i0e3	(a →0 (a ∩ b)) = (a →1 b)

Proof of Theorem lem3.3.7i0e3

Step	Hyp	Ref	Expression
1		nom10 307	1 (a →0 (a ∩ b)) = (a →1 b)

Syntax hints:   = wb 1   ∩ wa 7   →₀ wi0 11   →₁ wi1 12

This theorem was proved from axioms:  ax-a1 30  ax-r1 35  ax-r2 36

This theorem depends on definitions:  df-i0 43  df-i1 44

Copyright terms: Public domain