Theorem ifboth

Description: A wff th containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006) (Revised by Mario Carneiro, 15-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ifboth.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜃 ) )
2		ifboth.2	⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜒 ↔ 𝜃 ) )
3		simpll	⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜑 ) → 𝜓 )
4		simplr	⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ¬ 𝜑 ) → 𝜒 )
5	1 2 3 4	ifbothda	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )