Description: Theorem 19.43 of Margaris p. 90. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 27-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | 19.43 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-or | ||
2 | 1 | exbii | |
3 | 19.35 | ||
4 | alnex | ||
5 | 4 | imbi1i | |
6 | 2 3 5 | 3bitri | |
7 | df-or | ||
8 | 6 7 | bitr4i |