Theorem exbid 1104

Description: Formula-building rule for existential quantifier (deduction rule).

Hypotheses

Ref	Expression
exbid.1	|- (ph -> A.xph)
exbid.2	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
exbid	|- (ph -> (E.xps <-> E.xch))

Proof of Theorem exbid

Step	Hyp	Ref	Expression
1		exbid.1	. . 3 |- (ph -> A.xph)
2		exbid.2	. . 3 |- (ph -> (ps <-> ch))
3	1, 2	19.21ai 997	. 2 |- (ph -> A.x(ps <-> ch))
4		19.18 1049	. 2 |- (A.x(ps <-> ch) -> (E.xps <-> E.xch))
5	3, 4	syl 10	1 |- (ph -> (E.xps <-> E.xch))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 953  E.wex 979

This theorem is referenced by:  drex2 1156  exbidv 1278  mobid 1403  rexbida 1656  rexeq1f 1782  dfiun2g 2582  opabbid 2665  zfrepclf 2695  dfid3 2832  oprabbid 3990  axrepndlem1 4927  axrepndlem2 4928  axrepnd 4929  axunndlem1 4930  axpowndlem2 4933  axpowndlem3 4934  axpowndlem4 4935  axregnd 4939  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980

Copyright terms: Public domain