Description: 3impib with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bi23impib.1 | ||
Assertion | bi23impib |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi23impib.1 | ||
2 | 1 | biimpd | |
3 | 2 | 3impib |