Theorem ifpid2g

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

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

Proof

Step	Hyp	Ref	Expression
1		ifpidg	⊢ ( ( 𝜓 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ∧ ( 𝜓 → ( 𝜑 ∨ 𝜒 ) ) ) ) )
2		simpr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 )
3	2 2	pm3.2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) )
4	3	biantrur	⊢ ( ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ∧ ( 𝜓 → ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ∧ ( 𝜓 → ( 𝜑 ∨ 𝜒 ) ) ) ) )
5		ancom	⊢ ( ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ∧ ( 𝜓 → ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ( 𝜓 → ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ) )
6	1 4 5	3bitr2i	⊢ ( ( 𝜓 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( 𝜓 → ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ) )