Description: Theorem 19.15 of Margaris p. 90. (Contributed by NM, 24-Jan-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | albi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp | |
|
2 | 1 | al2imi | |
3 | biimpr | |
|
4 | 3 | al2imi | |
5 | 2 4 | impbid | |