Theorem ifbothda

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

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

Proof

Step	Hyp	Ref	Expression
1		ifboth.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜃 ) )
2		ifboth.2	⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜒 ↔ 𝜃 ) )
3		ifbothda.3	⊢ ( ( 𝜂 ∧ 𝜑 ) → 𝜓 )
4		ifbothda.4	⊢ ( ( 𝜂 ∧ ¬ 𝜑 ) → 𝜒 )
5		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
6	5	eqcomd	⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) )
7	6 1	syl	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜃 ) )
8	7	adantl	⊢ ( ( 𝜂 ∧ 𝜑 ) → ( 𝜓 ↔ 𝜃 ) )
9	3 8	mpbid	⊢ ( ( 𝜂 ∧ 𝜑 ) → 𝜃 )
10		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
11	10	eqcomd	⊢ ( ¬ 𝜑 → 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) )
12	11 2	syl	⊢ ( ¬ 𝜑 → ( 𝜒 ↔ 𝜃 ) )
13	12	adantl	⊢ ( ( 𝜂 ∧ ¬ 𝜑 ) → ( 𝜒 ↔ 𝜃 ) )
14	4 13	mpbid	⊢ ( ( 𝜂 ∧ ¬ 𝜑 ) → 𝜃 )
15	9 14	pm2.61dan	⊢ ( 𝜂 → 𝜃 )