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

Theorem bnj101 28426
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 1584 1  |-  E. x ps
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547
This theorem is referenced by:  bnj1023  28489  bnj1098  28492  bnj1101  28493  bnj1109  28495  bnj1468  28555  bnj1014  28669  bnj907  28674  bnj1110  28689  bnj1118  28691  bnj1128  28697  bnj1145  28700  bnj1172  28708  bnj1174  28710  bnj1176  28712
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator