Description: Constructor theorem for -/\ . (Contributed by Anthony Hart, 1-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | naim1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con3 | ||
2 | 1 | orim1d | |
3 | pm3.13 | ||
4 | pm3.14 | ||
5 | 3 4 | imim12i | |
6 | df-nan | ||
7 | df-nan | ||
8 | 5 6 7 | 3imtr4g | |
9 | 2 8 | syl |