Theorem ioin9i8

Description: Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022)

	Ref	Expression
Hypotheses	ioin9i8.1	$$⊢\phi \to \left(\psi \vee \chi \right)$$
	ioin9i8.2	$$⊢\chi \to \neg \theta$$
	ioin9i8.3	$$⊢\psi \to \theta$$
Assertion	ioin9i8	$$⊢\phi \to \left(\psi \leftrightarrow \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		ioin9i8.1	$$⊢\phi \to \left(\psi \vee \chi \right)$$
2		ioin9i8.2	$$⊢\chi \to \neg \theta$$
3		ioin9i8.3	$$⊢\psi \to \theta$$
4	1	ord	$$⊢\phi \to \left(\neg \psi \to \chi \right)$$
5	4 2	syl6	$$⊢\phi \to \left(\neg \psi \to \neg \theta \right)$$
6	5	con4d	$$⊢\phi \to \left(\theta \to \psi \right)$$
7	3 6	impbid2	$$⊢\phi \to \left(\psi \leftrightarrow \theta \right)$$