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

Theorem exim 1506
 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 1449 . 2 (∀𝑥(𝜑𝜓) → ∀𝑥𝑥(𝜑𝜓))
2 hbe1 1400 . 2 (∃𝑥𝜓 → ∀𝑥𝑥𝜓)
3 19.8a 1498 . . . 4 (𝜓 → ∃𝑥𝜓)
43imim2i 12 . . 3 ((𝜑𝜓) → (𝜑 → ∃𝑥𝜓))
54sps 1446 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∃𝑥𝜓))
61, 2, 5exlimdh 1503 1 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1257  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  eximi  1507  exbi  1511  eximdh  1518  19.29  1527  19.25  1533  alexim  1552  19.23t  1583  spimt  1640  equvini  1657  nfexd  1660  ax10oe  1694  sbcof2  1707  spsbim  1740  mor  1958  rexim  2430  elex22  2586  elex2  2587  vtoclegft  2642  spcimgft  2646  spcimegft  2648  spc2gv  2660  spc3gv  2662  ssoprab2  5588  bj-inf2vnlem1  10461
 Copyright terms: Public domain W3C validator