Theorem exbid 2265

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

Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1806  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfbidf  2266  drex2  2480  rexbida  3283  opabbid  5180  zfrepclf  5256  dfid3  5560  oprabbid  7476  axrepndlem1  10576  axrepndlem2  10577  axrepnd  10578  axpowndlem2  10582  axpowndlem3  10583  axpowndlem4  10584  axregnd  10588  axinfndlem1  10589  axinfnd  10590  axacndlem4  10594  axacndlem5  10595  axacnd  10596  opabdm  32896  opabrn  32897  axtcond  36877  pm14.122b  45024  pm14.123b  45027  modelaxreplem3  45580  alsbid  50464