Theorem bnj1419 13117

Description: First-order logic and set theory.

Hypotheses

Ref	Expression
bnj1419.1	|- (ph -> E.xps)
bnj1419.2	|- -. ps

Assertion

Ref	Expression
bnj1419	|- -. ph

Proof of Theorem bnj1419

Step	Hyp	Ref	Expression
1		bnj1419.2	. . 3 |- -. ps
2	1	nex 1456	. 2 |- -. E.xps
3		bnj1419.1	. 2 |- (ph -> E.xps)
4	2, 3	mto 121	1 |- -. ph

Syntax hints:  -. wn 2   -> wi 3  E.wex 1326

This theorem is referenced by:  bnj1523 13577

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

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

Copyright terms: Public domain