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	$$⊢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)$$
Assertion	ifboth	$$⊢\left(\psi \wedge \chi \right)\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		simpll	$$⊢\left(\left(\psi \wedge \chi \right)\wedge \phi \right)\to \psi$$
4		simplr	$$⊢\left(\left(\psi \wedge \chi \right)\wedge \neg \phi \right)\to \chi$$
5	1 2 3 4	ifbothda	$$⊢\left(\psi \wedge \chi \right)\to \theta$$