Theorem dfli2i 66

Description: Convert to linear implication. Inference for dfli2 64.

Hypothesis

Ref	Expression
dfli2i.1	⊦ (~ 𝜓 ⅋ 𝜒)

Assertion

Ref	Expression
dfli2i	⊦ (𝜓 ⊸ 𝜒)

Proof of Theorem dfli2i

Step	Hyp	Ref	Expression
1		dfli2i.1	. . . 4 ⊦ (~ 𝜓 ⅋ 𝜒)
2	1	ax-ibot 4	. . 3 ⊦ (⊥ ⅋ (~ 𝜓 ⅋ 𝜒))
3	2	dfli2 64	. 2 ⊦ (⊥ ⅋ (𝜓 ⊸ 𝜒))
4	3	ax-ebot 5	1 ⊦ (𝜓 ⊸ 𝜒)

Syntax hints:  ⊥wbot 1   ⅋ wmd 2  ~ wneg 3   ⊸ 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:  lb1s  67  lb2s  68  mdm1s  73  mdm2s  74  acm1s  84  acm2s  85  nems  86  dflb1s  91  dflb2s  92  licon  94  ilbd  97  lbsymd  102  mdco  108  mdas  110  md1  113  mcco  115  abs1  178