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

Theorem bnj593 28831
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 1582 . 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 1547
This theorem is referenced by:  bnj1266  28901  bnj1304  28909  bnj1379  28920  bnj594  29001  bnj852  29010  bnj908  29020  bnj981  29039  bnj996  29044  bnj907  29054  bnj1128  29077  bnj1148  29083  bnj1154  29086  bnj1189  29096  bnj1245  29101  bnj1279  29105  bnj1286  29106  bnj1311  29111  bnj1371  29116  bnj1398  29121  bnj1408  29123  bnj1450  29137  bnj1498  29148  bnj1514  29150  bnj1501  29154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator