Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj593 Structured version   Visualization version   GIF version

Theorem bnj593 31921
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj593.1 (𝜑 → ∃𝑥𝜓)
bnj593.2 (𝜓𝜒)
Assertion
Ref Expression
bnj593 (𝜑 → ∃𝑥𝜒)

Proof of Theorem bnj593
StepHypRef Expression
1 bnj593.1 . 2 (𝜑 → ∃𝑥𝜓)
2 bnj593.2 . . 3 (𝜓𝜒)
32eximi 1828 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-ex 1774
This theorem is referenced by:  bnj1266  31988  bnj1304  31996  bnj1379  32007  bnj594  32089  bnj852  32098  bnj908  32108  bnj996  32132  bnj907  32142  bnj1128  32165  bnj1148  32171  bnj1154  32174  bnj1189  32184  bnj1245  32189  bnj1279  32193  bnj1286  32194  bnj1311  32199  bnj1371  32204  bnj1398  32209  bnj1408  32211  bnj1450  32225  bnj1498  32236  bnj1514  32238  bnj1501  32242
  Copyright terms: Public domain W3C validator