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 31286
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 1929 . 2 (∃𝑥𝜓 → ∃𝑥𝜒)
41, 3syl 17 1 (𝜑 → ∃𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-ex 1875
This theorem is referenced by:  bnj1266  31353  bnj1304  31361  bnj1379  31372  bnj594  31453  bnj852  31462  bnj908  31472  bnj996  31496  bnj907  31506  bnj1128  31529  bnj1148  31535  bnj1154  31538  bnj1189  31548  bnj1245  31553  bnj1279  31557  bnj1286  31558  bnj1311  31563  bnj1371  31568  bnj1398  31573  bnj1408  31575  bnj1450  31589  bnj1498  31600  bnj1514  31602  bnj1501  31606
  Copyright terms: Public domain W3C validator