Theorem exbid 1964

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668

This theorem is referenced by:  mobid  2318  rexbida  2896  rexeqf  2984  opabbid  4465  zfrepclf  4521  dfid3  4750  oprabbid  6344  axrepndlem1  9017  axrepndlem2  9018  axrepnd  9019  axpowndlem2  9023  axpowndlem3  9024  axpowndlem4  9025  axregnd  9029  axinfndlem1  9030  axinfnd  9031  axacndlem4  9035  axacndlem5  9036  axacnd  9037  opabdm  28219  opabrn  28220  pm14.122b  36774  pm14.123b  36777