Metamath Proof Explorer


Theorem dfifp5

Description: Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019)

Ref Expression
Assertion dfifp5 ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( ¬ 𝜑𝜓 ) ∧ ( ¬ 𝜑𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 dfifp2 ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑𝜓 ) ∧ ( ¬ 𝜑𝜒 ) ) )
2 imor ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜓 ) )
3 2 anbi1i ( ( ( 𝜑𝜓 ) ∧ ( ¬ 𝜑𝜒 ) ) ↔ ( ( ¬ 𝜑𝜓 ) ∧ ( ¬ 𝜑𝜒 ) ) )
4 1 3 bitri ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( ¬ 𝜑𝜓 ) ∧ ( ¬ 𝜑𝜒 ) ) )