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 | |
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 | |