Theorem lbi2s 88

Description: Extract reverse implication from biconditional. Syllogism form of lb2i 60.

Assertion

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

Proof of Theorem lbi2s

Step	Hyp	Ref	Expression
1		df-lb 56	. . . . 5 ⊦ ((~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))) & (~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋ (𝜑 ⧟ 𝜓)))
2	1	eac1i 38	. . . 4 ⊦ (~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)))
3	2	ax-eac2 34	. . 3 ⊦ (~ (𝜑 ⧟ 𝜓) ⅋ (~ 𝜓 ⅋ 𝜑))
4		df-li 62	. . . 4 ⊦ ((𝜓 ⊸ 𝜑) ⧟ (~ 𝜓 ⅋ 𝜑))
5		df-lb 56	. . . . . 6 ⊦ ((~ ((𝜓 ⊸ 𝜑) ⧟ (~ 𝜓 ⅋ 𝜑)) ⅋ ((~ (𝜓 ⊸ 𝜑) ⅋ (~ 𝜓 ⅋ 𝜑)) & (~ (~ 𝜓 ⅋ 𝜑) ⅋ (𝜓 ⊸ 𝜑)))) & (~ ((~ (𝜓 ⊸ 𝜑) ⅋ (~ 𝜓 ⅋ 𝜑)) & (~ (~ 𝜓 ⅋ 𝜑) ⅋ (𝜓 ⊸ 𝜑))) ⅋ ((𝜓 ⊸ 𝜑) ⧟ (~ 𝜓 ⅋ 𝜑))))
6	5	eac1i 38	. . . . 5 ⊦ (~ ((𝜓 ⊸ 𝜑) ⧟ (~ 𝜓 ⅋ 𝜑)) ⅋ ((~ (𝜓 ⊸ 𝜑) ⅋ (~ 𝜓 ⅋ 𝜑)) & (~ (~ 𝜓 ⅋ 𝜑) ⅋ (𝜓 ⊸ 𝜑))))
7	6	ax-eac2 34	. . . 4 ⊦ (~ ((𝜓 ⊸ 𝜑) ⧟ (~ 𝜓 ⅋ 𝜑)) ⅋ (~ (~ 𝜓 ⅋ 𝜑) ⅋ (𝜓 ⊸ 𝜑)))
8	4, 7	cut1 10	. . 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:  lbi2  90  dflb1s  91