Theorem ifpid3g

Description: Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020)

	Ref	Expression
Assertion	ifpid3g	⊢ ( ( 𝜒 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜒 ) → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		olc	⊢ ( 𝜒 → ( 𝜑 ∨ 𝜒 ) )
2	1 1	pm3.2i	⊢ ( ( 𝜒 → ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜒 ) ) )
3		ifpidg	⊢ ( ( 𝜒 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜒 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜒 ) ) ) ) )
4	2 3	mpbiran2	⊢ ( ( 𝜒 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜒 ) → 𝜓 ) ) )