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

Theorem exim 1561
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 1503 . 2 (∀𝑥(𝜑𝜓) → ∀𝑥𝑥(𝜑𝜓))
2 hbe1 1454 . 2 (∃𝑥𝜓 → ∀𝑥𝑥𝜓)
3 19.8a 1552 . . . 4 (𝜓 → ∃𝑥𝜓)
43imim2i 12 . . 3 ((𝜑𝜓) → (𝜑 → ∃𝑥𝜓))
54sps 1500 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∃𝑥𝜓))
61, 2, 5exlimdh 1558 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1312  wex 1451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  eximi  1562  exbi  1566  eximdh  1573  19.29  1582  19.25  1588  alexim  1607  19.23t  1638  spimt  1697  equvini  1714  nfexd  1717  ax10oe  1751  sbcof2  1764  spsbim  1797  mor  2017  rexim  2501  elex22  2673  elex2  2674  vtoclegft  2730  spcimgft  2734  spcimegft  2736  spc2gv  2748  spc3gv  2750  ssoprab2  5793  bj-inf2vnlem1  13002
  Copyright terms: Public domain W3C validator