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	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
	ioin9i8.2	⊢ ( 𝜒 → ¬ 𝜃 )
	ioin9i8.3	⊢ ( 𝜓 → 𝜃 )
Assertion	ioin9i8	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		ioin9i8.1	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
2		ioin9i8.2	⊢ ( 𝜒 → ¬ 𝜃 )
3		ioin9i8.3	⊢ ( 𝜓 → 𝜃 )
4	1	ord	⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) )
5	4 2	syl6	⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ 𝜃 ) )
6	5	con4d	⊢ ( 𝜑 → ( 𝜃 → 𝜓 ) )
7	3 6	impbid2	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜃 ) )