Description: Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse . This is essentially dedlemb . (Contributed by BJ, 20-Sep-2019) (Proof shortened by Wolf Lammen, 25-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | ifpfal | ⊢ ( ¬ 𝜑 → ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifpn | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( ¬ 𝜑 , 𝜒 , 𝜓 ) ) | |
2 | ifptru | ⊢ ( ¬ 𝜑 → ( if- ( ¬ 𝜑 , 𝜒 , 𝜓 ) ↔ 𝜒 ) ) | |
3 | 1 2 | syl5bb | ⊢ ( ¬ 𝜑 → ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ 𝜒 ) ) |