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 29187
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 1586 . 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 1551
This theorem is referenced by:  bnj1266  29257  bnj1304  29265  bnj1379  29276  bnj594  29357  bnj852  29366  bnj908  29376  bnj981  29395  bnj996  29400  bnj907  29410  bnj1128  29433  bnj1148  29439  bnj1154  29442  bnj1189  29452  bnj1245  29457  bnj1279  29461  bnj1286  29462  bnj1311  29467  bnj1371  29472  bnj1398  29477  bnj1408  29479  bnj1450  29493  bnj1498  29504  bnj1514  29506  bnj1501  29510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator