Theorem lbi1s 87

Description: Extract forward implication from biconditional. Syllogism form of lb1i 59.

Assertion

Ref	Expression
lbi1s	⊦ ((𝜑 ⧟ 𝜓) ⊸ (𝜑 ⊸ 𝜓))

Proof of Theorem lbi1s

Step	Hyp	Ref	Expression
1		df-lb 56	. . . . 5 ⊦ ((~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))) & (~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋ (𝜑 ⧟ 𝜓)))
2	1	eac1i 38	. . . 4 ⊦ (~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)))
3	2	ax-eac1 33	. . 3 ⊦ (~ (𝜑 ⧟ 𝜓) ⅋ (~ 𝜑 ⅋ 𝜓))
4		df-li 62	. . . . 5 ⊦ ((𝜑 ⊸ 𝜓) ⧟ (~ 𝜑 ⅋ 𝜓))
5		df-lb 56	. . . . . 6 ⊦ ((~ ((𝜑 ⊸ 𝜓) ⧟ (~ 𝜑 ⅋ 𝜓)) ⅋ ((~ (𝜑 ⊸ 𝜓) ⅋ (~ 𝜑 ⅋ 𝜓)) & (~ (~ 𝜑 ⅋ 𝜓) ⅋ (𝜑 ⊸ 𝜓)))) & (~ ((~ (𝜑 ⊸ 𝜓) ⅋ (~ 𝜑 ⅋ 𝜓)) & (~ (~ 𝜑 ⅋ 𝜓) ⅋ (𝜑 ⊸ 𝜓))) ⅋ ((𝜑 ⊸ 𝜓) ⧟ (~ 𝜑 ⅋ 𝜓))))
6	5	eac1i 38	. . . . 5 ⊦ (~ ((𝜑 ⊸ 𝜓) ⧟ (~ 𝜑 ⅋ 𝜓)) ⅋ ((~ (𝜑 ⊸ 𝜓) ⅋ (~ 𝜑 ⅋ 𝜓)) & (~ (~ 𝜑 ⅋ 𝜓) ⅋ (𝜑 ⊸ 𝜓))))
7	4, 6	cut1 10	. . . 4 ⊦ ((~ (𝜑 ⊸ 𝜓) ⅋ (~ 𝜑 ⅋ 𝜓)) & (~ (~ 𝜑 ⅋ 𝜓) ⅋ (𝜑 ⊸ 𝜓)))
8	7	eac2i 40	. . 3 ⊦ (~ (~ 𝜑 ⅋ 𝜓) ⅋ (𝜑 ⊸ 𝜓))
9	3, 8	ax-cut 6	. 2 ⊦ (~ (𝜑 ⧟ 𝜓) ⅋ (𝜑 ⊸ 𝜓))
10		df-li 62	. 2 ⊦ (((𝜑 ⧟ 𝜓) ⊸ (𝜑 ⊸ 𝜓)) ⧟ (~ (𝜑 ⧟ 𝜓) ⅋ (𝜑 ⊸ 𝜓)))
11	9, 10	lb2i 60	1 ⊦ ((𝜑 ⧟ 𝜓) ⊸ (𝜑 ⊸ 𝜓))

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

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  df-li 62

This theorem is referenced by:  lbi1  89  dflb1s  91