This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Propositional calculus The conditional operator for propositions ifpimpda
Description: Separation of the values of the conditional operator for propositions.
(Contributed by AV , 30-Dec-2020) (Proof shortened by Wolf Lammen , 27-Feb-2021)
Ref
Expression
Hypotheses
ifpimpda.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
ifpimpda.2 ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜃 )
Assertion
ifpimpda ⊢ ( 𝜑 → if- ( 𝜓 , 𝜒 , 𝜃 ) )
Proof
Step
Hyp
Ref
Expression
1
ifpimpda.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2
ifpimpda.2 ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜃 )
3
1
ex ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
4
2
ex ⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜃 ) )
5
dfifp2 ⊢ ( if- ( 𝜓 , 𝜒 , 𝜃 ) ↔ ( ( 𝜓 → 𝜒 ) ∧ ( ¬ 𝜓 → 𝜃 ) ) )
6
3 4 5
sylanbrc ⊢ ( 𝜑 → if- ( 𝜓 , 𝜒 , 𝜃 ) )