Theorem dflb 93

Description: Nicer definition of biconditional. Uses ⧟ and ⊸.

Assertion

Ref	Expression
dflb	⊦ ((𝜑 ⧟ 𝜓) ⧟ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)))

Proof of Theorem dflb

Step	Hyp	Ref	Expression
1		dflb1s 91	. . 3 ⊦ ((𝜑 ⧟ 𝜓) ⊸ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)))
2		dflb2s 92	. . 3 ⊦ (((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)) ⊸ (𝜑 ⧟ 𝜓))
3	1, 2	iaci 36	. 2 ⊦ (((𝜑 ⧟ 𝜓) ⊸ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑))) & (((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)) ⊸ (𝜑 ⧟ 𝜓)))
4		dflb2s 92	. 2 ⊦ ((((𝜑 ⧟ 𝜓) ⊸ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑))) & (((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)) ⊸ (𝜑 ⧟ 𝜓))) ⊸ ((𝜑 ⧟ 𝜓) ⧟ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑))))
5	3, 4	lmp 76	1 ⊦ ((𝜑 ⧟ 𝜓) ⧟ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)))

Syntax hints:   & 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-mdas 9  ax-iac 32  ax-eac1 33  ax-eac2 34

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

This theorem is referenced by:  ilb  96  ilbd  97  lbsymd  102  abs1  178