Theorem lb2i 60

Description: Reverse inference using ⧟.

Hypotheses

Ref	Expression
lb2i.1	⊦ 𝜓
lb2i.2	⊦ (𝜑 ⧟ 𝜓)

Assertion

Ref	Expression
lb2i	⊦ 𝜑

Proof of Theorem lb2i

Step	Hyp	Ref	Expression
1		lb2i.1	. . . 4 ⊦ 𝜓
2	1	ax-ibot 4	. . 3 ⊦ (⊥ ⅋ 𝜓)
3		lb2i.2	. . 3 ⊦ (𝜑 ⧟ 𝜓)
4	2, 3	lb2d 58	. 2 ⊦ (⊥ ⅋ 𝜑)
5	4	ax-ebot 5	1 ⊦ 𝜑

Syntax hints:  ⊥wbot 1   ⧟ 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:  syl  75  id  77  dnis  78  dnes  79  lbi1s  87  lbi2s  88  ilb  96  abs1  178