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

Theorem bnj593 29040
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 1585 . 2  |-  ( E. x ps  ->  E. x ch )
41, 3syl 16 1  |-  ( ph  ->  E. x ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  bnj1266  29110  bnj1304  29118  bnj1379  29129  bnj594  29210  bnj852  29219  bnj908  29229  bnj981  29248  bnj996  29253  bnj907  29263  bnj1128  29286  bnj1148  29292  bnj1154  29295  bnj1189  29305  bnj1245  29310  bnj1279  29314  bnj1286  29315  bnj1311  29320  bnj1371  29325  bnj1398  29330  bnj1408  29332  bnj1450  29346  bnj1498  29357  bnj1514  29359  bnj1501  29363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator