Theorem bnj1369 13093

Description: First-order logic and set theory.

Hypotheses

Ref	Expression
bnj1369.1	|- (ph <-> (ps /\ ch))
bnj1369.2	|- (th -> E.xph)

Assertion

Ref	Expression
bnj1369	|- (th -> E.xps)

Proof of Theorem bnj1369

Step	Hyp	Ref	Expression
1		bnj1369.2	. . 3 |- (th -> E.xph)
2		bnj1369.1	. . . 4 |- (ph <-> (ps /\ ch))
3	2	exbii 1398	. . 3 |- (E.xph <-> E.x(ps /\ ch))
4	1, 3	sylib 215	. 2 |- (th -> E.x(ps /\ ch))
5		bnj1237 13005	. 2 |- (E.x(ps /\ ch) -> E.xps)
6	4, 5	syl 12	1 |- (th -> E.xps)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  E.wex 1326

This theorem is referenced by:  bnj1370 13094  bnj1371 13505  bnj1374 13508

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain