Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj593 Unicode version

Theorem bnj593 28774
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj593.1  |-  ( ph  ->  E. x ps )
bnj593.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
bnj593  |-  ( ph  ->  E. x ch )

Proof of Theorem bnj593
StepHypRef Expression
1 bnj593.1 . 2  |-  ( ph  ->  E. x ps )
2 bnj593.2 . . 3  |-  ( ps 
->  ch )
32eximi 1563 . 2  |-  ( E. x ps  ->  E. x ch )
41, 3syl 15 1  |-  ( ph  ->  E. x ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  bnj1266  28844  bnj1304  28852  bnj1379  28863  bnj594  28944  bnj852  28953  bnj908  28963  bnj981  28982  bnj996  28987  bnj907  28997  bnj1128  29020  bnj1148  29026  bnj1154  29029  bnj1189  29039  bnj1245  29044  bnj1279  29048  bnj1286  29049  bnj1311  29054  bnj1371  29059  bnj1398  29064  bnj1408  29066  bnj1450  29080  bnj1498  29091  bnj1514  29093  bnj1501  29097
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator