Theorem lb2d 58

Description: Reverse deduction using ⧟.

Hypotheses

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

Assertion

Ref	Expression
lb2d	⊦ (𝜑 ⅋ 𝜓)

Proof of Theorem lb2d

Step	Hyp	Ref	Expression
1		lb2d.1	. 2 ⊦ (𝜑 ⅋ 𝜒)
2		lb2d.2	. . . 4 ⊦ (𝜓 ⧟ 𝜒)
3		df-lb 56	. . . . 5 ⊦ ((~ (𝜓 ⧟ 𝜒) ⅋ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓))) & (~ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓)) ⅋ (𝜓 ⧟ 𝜒)))
4	3	eac1i 38	. . . 4 ⊦ (~ (𝜓 ⧟ 𝜒) ⅋ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓)))
5	2, 4	cut1 10	. . 3 ⊦ ((~ 𝜓 ⅋ 𝜒) & (~ 𝜒 ⅋ 𝜓))
6	5	eac2i 40	. 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  ax-eac2 34

This theorem depends on definitions:  df-lb 56

This theorem is referenced by:  lb2i  60  dfli2  64  lb2s  68  ilbd  97