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 34760
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 1834 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ex 1779
This theorem is referenced by:  bnj1266  34826  bnj1304  34834  bnj1379  34845  bnj594  34927  bnj852  34936  bnj908  34946  bnj996  34971  bnj907  34982  bnj1128  35005  bnj1148  35011  bnj1154  35014  bnj1189  35024  bnj1245  35029  bnj1279  35033  bnj1286  35034  bnj1311  35039  bnj1371  35044  bnj1398  35049  bnj1408  35051  bnj1450  35065  bnj1498  35076  bnj1514  35078  bnj1501  35082
  Copyright terms: Public domain W3C validator