Metamath Proof Explorer


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 φψθ