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	$$⊢A=if\left(\phi ,A,B\right)\to \left(\psi \leftrightarrow \theta \right)$$
	ifboth.2	$$⊢B=if\left(\phi ,A,B\right)\to \left(\chi \leftrightarrow \theta \right)$$
	ifbothda.3	$$⊢\left(\eta \wedge \phi \right)\to \psi$$
	ifbothda.4	$$⊢\left(\eta \wedge \neg \phi \right)\to \chi$$
Assertion	ifbothda	$$⊢\eta \to \theta$$

Proof

Step	Hyp	Ref	Expression
1		ifboth.1	$$⊢A=if\left(\phi ,A,B\right)\to \left(\psi \leftrightarrow \theta \right)$$
2		ifboth.2	$$⊢B=if\left(\phi ,A,B\right)\to \left(\chi \leftrightarrow \theta \right)$$
3		ifbothda.3	$$⊢\left(\eta \wedge \phi \right)\to \psi$$
4		ifbothda.4	$$⊢\left(\eta \wedge \neg \phi \right)\to \chi$$
5		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
6	5	eqcomd	$$⊢\phi \to A=if\left(\phi ,A,B\right)$$
7	6 1	syl	$$⊢\phi \to \left(\psi \leftrightarrow \theta \right)$$
8	7	adantl	$$⊢\left(\eta \wedge \phi \right)\to \left(\psi \leftrightarrow \theta \right)$$
9	3 8	mpbid	$$⊢\left(\eta \wedge \phi \right)\to \theta$$
10		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
11	10	eqcomd	$$⊢\neg \phi \to B=if\left(\phi ,A,B\right)$$
12	11 2	syl	$$⊢\neg \phi \to \left(\chi \leftrightarrow \theta \right)$$
13	12	adantl	$$⊢\left(\eta \wedge \neg \phi \right)\to \left(\chi \leftrightarrow \theta \right)$$
14	4 13	mpbid	$$⊢\left(\eta \wedge \neg \phi \right)\to \theta$$
15	9 14	pm2.61dan	$$⊢\eta \to \theta$$