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

Theorem bnj101 28822
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 1565 . 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 1530
This theorem is referenced by:  bnj1023  28885  bnj1098  28888  bnj1101  28889  bnj1109  28891  bnj1468  28951  bnj1014  29065  bnj907  29070  bnj1110  29085  bnj1118  29087  bnj1128  29093  bnj1145  29096  bnj1172  29104  bnj1174  29106  bnj1176  29108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546
This theorem depends on definitions:  df-bi 177  df-ex 1531
  Copyright terms: Public domain W3C validator