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	|- ( ph -> ( ps \/ ch ) )
	ioin9i8.2	|- ( ch -> -. th )
	ioin9i8.3	|- ( ps -> th )
Assertion	ioin9i8	|- ( ph -> ( ps <-> th ) )

Proof

Step	Hyp	Ref	Expression
1		ioin9i8.1	|- ( ph -> ( ps \/ ch ) )
2		ioin9i8.2	|- ( ch -> -. th )
3		ioin9i8.3	|- ( ps -> th )
4	1	ord	|- ( ph -> ( -. ps -> ch ) )
5	4 2	syl6	|- ( ph -> ( -. ps -> -. th ) )
6	5	con4d	|- ( ph -> ( th -> ps ) )
7	3 6	impbid2	|- ( ph -> ( ps <-> th ) )