Axiom ax-cut 6

Description: The cut rule is akin to syllogism in classical logic. It allows ~ 𝜑 ⅋ 𝜓 to act like an implication, so that an 𝜑 can be removed and traded for a 𝜓.

Hypotheses

Ref	Expression
ax-cut.1	⊦ (𝜑 ⅋ 𝜓)
ax-cut.2	⊦ (~ 𝜓 ⅋ 𝜒)

Assertion

Ref	Expression
ax-cut	⊦ (𝜑 ⅋ 𝜒)

Detailed syntax breakdown of Axiom ax-cut

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wch	. 2 wff 𝜒
3	1, 2	wmd 2	1 wff (𝜑 ⅋ 𝜒)

This axiom is referenced by:  cut1  10  mdcod  11  mdasd  13  mdasr  15  mdasrd  16  cutneg  21  cutf  22  dnid  23  dned  24  lb1d  57  lb2d  58  mdm2  69  syl  75  dnes  79  nems  86  lbi1s  87  lbi2s  88