Theorem iotabii 6548

Description: Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)

Hypothesis

Ref	Expression
iotabii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
iotabii	⊢ (℩𝑥𝜑) = (℩𝑥𝜓)

Proof of Theorem iotabii

Step	Hyp	Ref	Expression
1		iotabi 6529	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
2		iotabii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1794	1 ⊢ (℩𝑥𝜑) = (℩𝑥𝜓)

Syntax hints:   ↔ wb 206   = wceq 1537  ℩cio 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-iota 6516

This theorem is referenced by:  riotav  7393  riotarab  7430  ovtpos  8265  cbvsum  15728  cbvsumv  15729  cbvprod  15946  cbvprodv  15947  prodeq1i  15949  oppgid  19390  oppr1  20367  riotaeqbii  36180  sumeq2si  36184  prodeq2si  36186  cbvprodvw2  36230  fourierdlem89  46151  fourierdlem90  46152  fourierdlem91  46153  fourierdlem96  46158  fourierdlem97  46159  fourierdlem98  46160  fourierdlem99  46161  fourierdlem100  46162  fourierdlem112  46174