Theorem exbid 2237

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 2209	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		albid.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	exbidh 1875	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 208  ∃wex 1787  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfbidf  2238  drex2  2452  rexbida  3253  opabbid  5140  zfrepclf  5216  dfid3  5519  oprabbid  7425  axrepndlem1  10510  axrepndlem2  10511  axrepnd  10512  axpowndlem2  10516  axpowndlem3  10517  axpowndlem4  10518  axregnd  10522  axinfndlem1  10523  axinfnd  10524  axacndlem4  10528  axacndlem5  10529  axacnd  10530  opabdm  32707  opabrn  32708  axtcond  36721  pm14.122b  44882  pm14.123b  44885  modelaxreplem3  45439