Theorem exbid 1984

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 1972	. 2 |- ( ph -> A. x ph )
3		exbid.2	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	exbidh 1735	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

Syntax hints:   -> wi 4   <-> wb 189   E.wex 1671   F/wnf 1675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676

This theorem is referenced by:  mobid  2338  rexbida  2887  rexeqf  2970  opabbid  4458  zfrepclf  4514  dfid3  4755  oprabbid  6363  axrepndlem1  9035  axrepndlem2  9036  axrepnd  9037  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axregnd  9047  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  opabdm  28295  opabrn  28296  pm14.122b  36844  pm14.123b  36847