Description: The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp . (Contributed by BJ, 1-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | ifpor | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) → ( 𝜓 ∨ 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ifp | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ) | |
2 | simpr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) | |
3 | simpr | ⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜒 ) | |
4 | 2 3 | orim12i | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → ( 𝜓 ∨ 𝜒 ) ) |
5 | 1 4 | sylbi | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) → ( 𝜓 ∨ 𝜒 ) ) |