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

Metamath Proof Explorer

Theorem binom2d

Description: Deduction form of binom2 . (Contributed by Igor Ieskov, 14-Dec-2023)

Ref Expression
Hypotheses binom2d.1 ⊢ φ → A ∈ ℂ
binom2d.2 ⊢ φ → B ∈ ℂ
Assertion binom2d ⊢ φ → A + B 2 = A 2 + 2 ⁢ A ⁢ B + B 2

Proof

Step Hyp Ref Expression
1 binom2d.1 ⊢ φ → A ∈ ℂ
2 binom2d.2 ⊢ φ → B ∈ ℂ
3 binom2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 = A 2 + 2 ⁢ A ⁢ B + B 2
4 1 2 3 syl2anc ⊢ φ → A + B 2 = A 2 + 2 ⁢ A ⁢ B + B 2