This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efsubd

Description: Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses efsubd.a ⊢ φ → A ∈ ℂ
efsubd.b ⊢ φ → B ∈ ℂ
Assertion efsubd ⊢ φ → e A − B = e A e B

Proof

Step Hyp Ref Expression
1 efsubd.a ⊢ φ → A ∈ ℂ
2 efsubd.b ⊢ φ → B ∈ ℂ
3 efsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → e A − B = e A e B
4 1 2 3 syl2anc ⊢ φ → e A − B = e A e B