Metamath Proof Explorer


Theorem ifpor

Description: The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp . (Contributed by BJ, 1-Oct-2019)

Ref Expression
Assertion ifpor ( if- ( 𝜑 , 𝜓 , 𝜒 ) → ( 𝜓𝜒 ) )

Proof

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