Description: Obsolete proof of 19.43 . Do not delete as it is referenced on the mmrecent.html page and in conventions-labels . (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 19.43OLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioran | |
|
2 | 1 | albii | |
3 | 19.26 | |
|
4 | alnex | |
|
5 | alnex | |
|
6 | 4 5 | anbi12i | |
7 | 2 3 6 | 3bitri | |
8 | 7 | notbii | |
9 | df-ex | |
|
10 | oran | |
|
11 | 8 9 10 | 3bitr4i | |