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 29551
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 1702 . 2  |-  ( E. x ps  ->  E. x ch )
41, 3syl 17 1  |-  ( ph  ->  E. x ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  bnj1266  29619  bnj1304  29627  bnj1379  29638  bnj594  29719  bnj852  29728  bnj908  29738  bnj996  29762  bnj907  29772  bnj1128  29795  bnj1148  29801  bnj1154  29804  bnj1189  29814  bnj1245  29819  bnj1279  29823  bnj1286  29824  bnj1311  29829  bnj1371  29834  bnj1398  29839  bnj1408  29841  bnj1450  29855  bnj1498  29866  bnj1514  29868  bnj1501  29872
  Copyright terms: Public domain W3C validator