Description: An exportation inference. (Contributed by NM, 26-Apr-1994) (Proof shortened by Wolf Lammen, 20-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | exp4a.1 | |
|
Assertion | exp4a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp4a.1 | |
|
2 | 1 | imp | |
3 | 2 | exp4b | |