Description: Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | dfifp5 | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfifp2 | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) | |
2 | imor | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) ) | |
3 | 2 | anbi1i | ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) |
4 | 1 3 | bitri | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) |