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

Theorem exlimi 1573
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exlimi.1 𝑥𝜓
exlimi.2 (𝜑𝜓)
Assertion
Ref Expression
exlimi (∃𝑥𝜑𝜓)

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3 𝑥𝜓
21nfri 1499 . 2 (𝜓 → ∀𝑥𝜓)
3 exlimi.2 . 2 (𝜑𝜓)
42, 3exlimih 1572 1 (∃𝑥𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  Ⅎwnf 1436  ∃wex 1468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470  ax-4 1487 This theorem depends on definitions:  df-bi 116  df-nf 1437 This theorem is referenced by:  19.36i  1650  euexex  2084  ceqsex  2724  sbhypf  2735  vtoclgf  2744  vtoclg1f  2745  vtoclef  2759  copsexg  4166  copsex2g  4168  ralxpf  4685  rexxpf  4686  dmcoss  4808  fv3  5444  tz6.12c  5451  0neqopab  5816  cnvoprab  6131  bj-exlimmpi  13061
 Copyright terms: Public domain W3C validator