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 30069
 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 1752 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  bnj1266  30136  bnj1304  30144  bnj1379  30155  bnj594  30236  bnj852  30245  bnj908  30255  bnj996  30279  bnj907  30289  bnj1128  30312  bnj1148  30318  bnj1154  30321  bnj1189  30331  bnj1245  30336  bnj1279  30340  bnj1286  30341  bnj1311  30346  bnj1371  30351  bnj1398  30356  bnj1408  30358  bnj1450  30372  bnj1498  30383  bnj1514  30385  bnj1501  30389
 Copyright terms: Public domain W3C validator