Theorem elimif

Description: Elimination of a conditional operator contained in a wff ps . (Contributed by NM, 15-Feb-2005) (Proof shortened by NM, 25-Apr-2019)

	Ref	Expression
Hypotheses	elimif.1	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
	elimif.2	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 → ( 𝜓 ↔ 𝜃 ) )
Assertion	elimif	⊢ ( 𝜓 ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( ¬ 𝜑 ∧ 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elimif.1	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
2		elimif.2	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 → ( 𝜓 ↔ 𝜃 ) )
3		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
4	3 1	syl	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
5		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
6	5 2	syl	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ 𝜃 ) )
7	4 6	cases	⊢ ( 𝜓 ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( ¬ 𝜑 ∧ 𝜃 ) ) )