Theorem exbid 2266

Description: Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
albid.1	⊢ Ⅎ𝑥𝜑
albid.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
exbid	⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Proof of Theorem exbid

Step	Hyp	Ref	Expression
1		albid.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nf5ri 2236	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		albid.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	exbidh 1968	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 198  ∃wex 1878  Ⅎwnf 1882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-12 2220

This theorem depends on definitions:  df-bi 199  df-ex 1879  df-nf 1883

This theorem is referenced by:  nfbidf  2267  drex2  2463  eubidOLD  2661  mobidOLDOLD  2681  rexbida  3257  rexeqf  3347  opabbid  4940  zfrepclf  5003  dfid3  5253  oprabbid  6973  axrepndlem1  9736  axrepndlem2  9737  axrepnd  9738  axpowndlem2  9742  axpowndlem3  9743  axpowndlem4  9744  axregnd  9748  axinfndlem1  9749  axinfnd  9750  axacndlem4  9754  axacndlem5  9755  axacnd  9756  opabdm  29966  opabrn  29967  pm14.122b  39462  pm14.123b  39465