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 32037
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 1626 . 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 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  bnj1266  32105  bnj1304  32113  bnj1379  32124  bnj594  32205  bnj852  32214  bnj908  32224  bnj981  32243  bnj996  32248  bnj907  32258  bnj1128  32281  bnj1148  32287  bnj1154  32290  bnj1189  32300  bnj1245  32305  bnj1279  32309  bnj1286  32310  bnj1311  32315  bnj1371  32320  bnj1398  32325  bnj1408  32327  bnj1450  32341  bnj1498  32352  bnj1514  32354  bnj1501  32358
  Copyright terms: Public domain W3C validator