Metamath Proof Explorer


Theorem 1fpid3

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- ( 𝜑 , 𝜓 , 𝜒 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 1fpid3.1 ( ( 𝜑𝜓 ) → 𝜒 )
2 df-ifp ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑𝜓 ) ∨ ( ¬ 𝜑𝜒 ) ) )
3 simpr ( ( ¬ 𝜑𝜒 ) → 𝜒 )
4 1 3 jaoi ( ( ( 𝜑𝜓 ) ∨ ( ¬ 𝜑𝜒 ) ) → 𝜒 )
5 2 4 sylbi ( if- ( 𝜑 , 𝜓 , 𝜒 ) → 𝜒 )