Theorem lb1d 57

Description: Forward deduction using ⧟.

Hypotheses

Ref	Expression
lb1d.1	⊦ (𝜑 ⅋ 𝜓)
lb1d.2	⊦ (𝜓 ⧟ 𝜒)

Assertion

Ref	Expression
lb1d	⊦ (𝜑 ⅋ 𝜒)

Proof of Theorem lb1d

Step	Hyp	Ref	Expression
1		lb1d.1	. 2 ⊦ (𝜑 ⅋ 𝜓)
2		lb1d.2	. . . 4 ⊦ (𝜓 ⧟ 𝜒)
3		df-lb 56	. . . . 5 ⊦ ((~ (𝜓 ⧟ 𝜒) ⅋ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓))) & (~ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓)) ⅋ (𝜓 ⧟ 𝜒)))
4	3	eac1i 38	. . . 4 ⊦ (~ (𝜓 ⧟ 𝜒) ⅋ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓)))
5	2, 4	cut1 10	. . 3 ⊦ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓))
6	5	eac1i 38	. 2 ⊦ (~ 𝜓 ⅋ 𝜒)
7	1, 6	ax-cut 6	1 ⊦ (𝜑 ⅋ 𝜒)

Syntax hints:   ⅋ wmd 2  ~ wneg 3   & wac 30   ⧟ wlb 55

This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-init 7  ax-mdco 8  ax-eac1 33

This theorem depends on definitions:  df-lb 56

This theorem is referenced by:  lb1i  59  dfli1  63  lb1s  67  lbsymd  102