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 30789
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 1760 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  bnj1266  30856  bnj1304  30864  bnj1379  30875  bnj594  30956  bnj852  30965  bnj908  30975  bnj996  30999  bnj907  31009  bnj1128  31032  bnj1148  31038  bnj1154  31041  bnj1189  31051  bnj1245  31056  bnj1279  31060  bnj1286  31061  bnj1311  31066  bnj1371  31071  bnj1398  31076  bnj1408  31078  bnj1450  31092  bnj1498  31103  bnj1514  31105  bnj1501  31109
  Copyright terms: Public domain W3C validator