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 32758
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 1630 . 2  |-  ( E. x ps  ->  E. x ch )
41, 3syl 16 1  |-  ( ph  ->  E. x ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607
This theorem depends on definitions:  df-bi 185  df-ex 1592
This theorem is referenced by:  bnj1266  32826  bnj1304  32834  bnj1379  32845  bnj594  32926  bnj852  32935  bnj908  32945  bnj981  32964  bnj996  32969  bnj907  32979  bnj1128  33002  bnj1148  33008  bnj1154  33011  bnj1189  33021  bnj1245  33026  bnj1279  33030  bnj1286  33031  bnj1311  33036  bnj1371  33041  bnj1398  33046  bnj1408  33048  bnj1450  33062  bnj1498  33073  bnj1514  33075  bnj1501  33079
  Copyright terms: Public domain W3C validator