Theorem bnj1126 13703

Description: First-order logic and set theory.

Hypotheses

Ref	Expression
bnj1126.1	|- (ph -> ps)
bnj1126.2	|- E.x(ph -> (ps' <-> ps))

Assertion

Ref	Expression
bnj1126	|- E.x(ph -> ps')

Proof of Theorem bnj1126

Step	Hyp	Ref	Expression
1		bnj1126.2	. . 3 |- E.x(ph -> (ps' <-> ps))
2		bnj1126.1	. . 3 |- (ph -> ps)
3	1, 2	bnj1025 13651	. 2 |- E.x((ph -> ps) /\ (ph -> (ps' <-> ps)))
4		bi2 227	. . . 4 |- ((ps' <-> ps) -> (ps -> ps'))
5	4	imim2i 12	. . 3 |- ((ph -> (ps' <-> ps)) -> (ph -> (ps -> ps')))
6		ax-2 5	. . . 4 |- ((ph -> (ps -> ps')) -> ((ph -> ps) -> (ph -> ps')))
7	6	impcom 394	. . 3 |- (((ph -> ps) /\ (ph -> (ps -> ps'))) -> (ph -> ps'))
8	5, 7	sylan2 600	. 2 |- (((ph -> ps) /\ (ph -> (ps' <-> ps))) -> (ph -> ps'))
9	3, 8	bnj101 13232	1 |- E.x(ph -> ps')

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337  E.wex 1615

This theorem is referenced by:  bnj1130 13704

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1593  ax-4 1608  ax-5o 1610

This theorem depends on definitions:  df-bi 220  df-an 339  df-ex 1616

Copyright terms: Public domain