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

Theorem bnj101 29065
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 1566 . 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 1531
This theorem is referenced by:  bnj1023  29128  bnj1098  29131  bnj1101  29132  bnj1109  29134  bnj1468  29194  bnj1014  29308  bnj907  29313  bnj1110  29328  bnj1118  29330  bnj1128  29336  bnj1145  29339  bnj1172  29347  bnj1174  29349  bnj1176  29351
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator