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 31153
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 1910 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  bnj1266  31220  bnj1304  31228  bnj1379  31239  bnj594  31320  bnj852  31329  bnj908  31339  bnj996  31363  bnj907  31373  bnj1128  31396  bnj1148  31402  bnj1154  31405  bnj1189  31415  bnj1245  31420  bnj1279  31424  bnj1286  31425  bnj1311  31430  bnj1371  31435  bnj1398  31440  bnj1408  31442  bnj1450  31456  bnj1498  31467  bnj1514  31469  bnj1501  31473
  Copyright terms: Public domain W3C validator