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

Theorem bnj593 28526
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 1581 . 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 1546
This theorem is referenced by:  bnj1266  28596  bnj1304  28604  bnj1379  28615  bnj594  28696  bnj852  28705  bnj908  28715  bnj981  28734  bnj996  28739  bnj907  28749  bnj1128  28772  bnj1148  28778  bnj1154  28781  bnj1189  28791  bnj1245  28796  bnj1279  28800  bnj1286  28801  bnj1311  28806  bnj1371  28811  bnj1398  28816  bnj1408  28818  bnj1450  28832  bnj1498  28843  bnj1514  28845  bnj1501  28849
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562
This theorem depends on definitions:  df-bi 177  df-ex 1547
  Copyright terms: Public domain W3C validator