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 31120
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 1909 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884
This theorem depends on definitions:  df-bi 197  df-ex 1852
This theorem is referenced by:  bnj1266  31187  bnj1304  31195  bnj1379  31206  bnj594  31287  bnj852  31296  bnj908  31306  bnj996  31330  bnj907  31340  bnj1128  31363  bnj1148  31369  bnj1154  31372  bnj1189  31382  bnj1245  31387  bnj1279  31391  bnj1286  31392  bnj1311  31397  bnj1371  31402  bnj1398  31407  bnj1408  31409  bnj1450  31423  bnj1498  31434  bnj1514  31436  bnj1501  31440
  Copyright terms: Public domain W3C validator