Theorem exbid 1939

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

Hypotheses

Ref	Expression
exbid.1	|- F/ x ph
exbid.2	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
exbid	|- ( ph -> ( E. x ps <-> E. x ch ) )

Proof of Theorem exbid

Step	Hyp	Ref	Expression
1		exbid.1	. . 3 |- F/ x ph
2	1	nfri 1927	. 2 |- ( ph -> A. x ph )
3		exbid.2	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	exbidh 1723	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

Syntax hints:   -> wi 4   <-> wb 187   E.wex 1659   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907

This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664

This theorem is referenced by:  mobid  2287  rexbida  2941  rexeqf  3029  opabbid  4488  zfrepclf  4544  dfid3  4770  oprabbid  6358  axrepndlem1  9015  axrepndlem2  9016  axrepnd  9017  axpowndlem2  9021  axpowndlem3  9022  axpowndlem4  9023  axregnd  9027  axregndOLD  9028  axinfndlem1  9029  axinfnd  9030  axacndlem4  9034  axacndlem5  9035  axacnd  9036  opabdm  28066  opabrn  28067  pm14.122b  36426  pm14.123b  36429