Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj101 Structured version   Unicode version

Theorem bnj101 29025
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj101.1  |-  E. x ph
bnj101.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
bnj101  |-  E. x ps

Proof of Theorem bnj101
StepHypRef Expression
1 bnj101.1 . 2  |-  E. x ph
2 bnj101.2 . 2  |-  ( ph  ->  ps )
31, 2eximii 1587 1  |-  E. x ps
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  bnj1023  29088  bnj1098  29091  bnj1101  29092  bnj1109  29094  bnj1468  29154  bnj1014  29268  bnj907  29273  bnj1110  29288  bnj1118  29290  bnj1128  29296  bnj1145  29299  bnj1172  29307  bnj1174  29309  bnj1176  29311
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator