Theorem mdm2 69

Description: Par is monotone in its second argument.

Hypotheses

Ref	Expression
mdm2.1	⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜓))
mdm2.2	⊦ (𝜓 ⊸ 𝜒)

Assertion

Ref	Expression
mdm2	⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜒))

Proof of Theorem mdm2

Step	Hyp	Ref	Expression
1		mdm2.1	. . . 4 ⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜓))
2	1	mdasri 17	. . 3 ⊦ ((𝜃 ⅋ 𝜑) ⅋ 𝜓)
3		mdm2.2	. . . 4 ⊦ (𝜓 ⊸ 𝜒)
4		df-li 62	. . . 4 ⊦ ((𝜓 ⊸ 𝜒) ⧟ (~ 𝜓 ⅋ 𝜒))
5	3, 4	lb1i 59	. . 3 ⊦ (~ 𝜓 ⅋ 𝜒)
6	2, 5	ax-cut 6	. 2 ⊦ ((𝜃 ⅋ 𝜑) ⅋ 𝜒)
7	6	mdasi 14	1 ⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜒))

Syntax hints:   ⅋ 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-mdas 9  ax-eac1 33

This theorem depends on definitions:  df-lb 56  df-li 62

This theorem is referenced by:  mdm1  70  mdm2i  72  mdm2s  74