Theorem exbid 2260

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

Syntax hints:   → wi 4   ↔ wb 208  ∃wex 1801  Ⅎwnf 1805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-ex 1802  df-nf 1806

This theorem is referenced by:  nfbidf  2261  drex2  2475  rexbida  3276  opabbid  5167  zfrepclf  5243  dfid3  5547  oprabbid  7463  axrepndlem1  10552  axrepndlem2  10553  axrepnd  10554  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axregnd  10564  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  opabdm  32815  opabrn  32816  axtcond  36843  pm14.122b  45004  pm14.123b  45007  modelaxreplem3  45561