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 33670
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 1643 . 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 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618
This theorem depends on definitions:  df-bi 185  df-ex 1600
This theorem is referenced by:  bnj1266  33738  bnj1304  33746  bnj1379  33757  bnj594  33838  bnj852  33847  bnj908  33857  bnj996  33881  bnj907  33891  bnj1128  33914  bnj1148  33920  bnj1154  33923  bnj1189  33933  bnj1245  33938  bnj1279  33942  bnj1286  33943  bnj1311  33948  bnj1371  33953  bnj1398  33958  bnj1408  33960  bnj1450  33974  bnj1498  33985  bnj1514  33987  bnj1501  33991
  Copyright terms: Public domain W3C validator