Description: The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 1fpid3.1 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) | |
Assertion | 1fpid3 | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) → 𝜒 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1fpid3.1 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) | |
2 | df-ifp | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ) | |
3 | simpr | ⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜒 ) | |
4 | 1 3 | jaoi | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → 𝜒 ) |
5 | 2 4 | sylbi | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) → 𝜒 ) |