Description: Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | ichim |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ichn | ||
2 | ichan | ||
3 | 1 2 | sylan2b | |
4 | ichn | ||
5 | 3 4 | sylib | |
6 | iman | ||
7 | 6 | a1i | |
8 | 7 | ichbidv | |
9 | 8 | mptru | |
10 | 5 9 | sylibr |