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 29862
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 1751 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  bnj1266  29929  bnj1304  29937  bnj1379  29948  bnj594  30029  bnj852  30038  bnj908  30048  bnj996  30072  bnj907  30082  bnj1128  30105  bnj1148  30111  bnj1154  30114  bnj1189  30124  bnj1245  30129  bnj1279  30133  bnj1286  30134  bnj1311  30139  bnj1371  30144  bnj1398  30149  bnj1408  30151  bnj1450  30165  bnj1498  30176  bnj1514  30178  bnj1501  30182
  Copyright terms: Public domain W3C validator