This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Closure law for the exponential function. (Contributed by NM, 8-Jan-2006) (Revised by Mario Carneiro, 10-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | efcl |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eff | ||
| 2 | 1 | ffvelcdmi |