ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exim GIF version

Theorem exim 1535
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
exim (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Proof of Theorem exim
StepHypRef Expression
1 hba1 1478 . 2 (∀𝑥(𝜑𝜓) → ∀𝑥𝑥(𝜑𝜓))
2 hbe1 1429 . 2 (∃𝑥𝜓 → ∀𝑥𝑥𝜓)
3 19.8a 1527 . . . 4 (𝜓 → ∃𝑥𝜓)
43imim2i 12 . . 3 ((𝜑𝜓) → (𝜑 → ∃𝑥𝜓))
54sps 1475 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∃𝑥𝜓))
61, 2, 5exlimdh 1532 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287  wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eximi  1536  exbi  1540  eximdh  1547  19.29  1556  19.25  1562  alexim  1581  19.23t  1612  spimt  1671  equvini  1688  nfexd  1691  ax10oe  1725  sbcof2  1738  spsbim  1771  mor  1990  rexim  2467  elex22  2634  elex2  2635  vtoclegft  2691  spcimgft  2695  spcimegft  2697  spc2gv  2709  spc3gv  2711  ssoprab2  5687  bj-inf2vnlem1  11522
  Copyright terms: Public domain W3C validator