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 29088
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  29151  bnj1098  29154  bnj1101  29155  bnj1109  29157  bnj1468  29217  bnj1014  29331  bnj907  29336  bnj1110  29351  bnj1118  29353  bnj1128  29359  bnj1145  29362  bnj1172  29370  bnj1174  29372  bnj1176  29374
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