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  5562  oprabbid  7478  axrepndlem1  10579  axrepndlem2  10580  axrepnd  10581  axpowndlem2  10585  axpowndlem3  10586  axpowndlem4  10587  axregnd  10591  axinfndlem1  10592  axinfnd  10593  axacndlem4  10597  axacndlem5  10598  axacnd  10599  opabdm  32899  opabrn  32900  axtcond  36914  pm14.122b  45062  pm14.123b  45065  modelaxreplem3  45618  alsbid  50502