Theorem ifpdfor2

Description: Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020)

	Ref	Expression
Assertion	ifpdfor2	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ if- ( 𝜑 , 𝜑 , 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.1	⊢ ( ¬ 𝜑 ∨ 𝜑 )
2	1	biantrur	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( ¬ 𝜑 ∨ 𝜑 ) ∧ ( 𝜑 ∨ 𝜓 ) ) )
3		dfifp4	⊢ ( if- ( 𝜑 , 𝜑 , 𝜓 ) ↔ ( ( ¬ 𝜑 ∨ 𝜑 ) ∧ ( 𝜑 ∨ 𝜓 ) ) )
4	2 3	bitr4i	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ if- ( 𝜑 , 𝜑 , 𝜓 ) )