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

Theorem bnj101 28749
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 . . 3  |-  ( ph  ->  ps )
32eximi 1563 . 2  |-  ( E. x ph  ->  E. x ps )
41, 3ax-mp 8 1  |-  E. x ps
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  bnj1023  28812  bnj1098  28815  bnj1101  28816  bnj1109  28818  bnj1468  28878  bnj1014  28992  bnj907  28997  bnj1110  29012  bnj1118  29014  bnj1128  29020  bnj1145  29023  bnj1172  29031  bnj1174  29033  bnj1176  29035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator