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

Theorem exim 1487
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 (x(φψ) → (xφxψ))

Proof of Theorem exim
StepHypRef Expression
1 hba1 1430 . 2 (x(φψ) → xx(φψ))
2 hbe1 1381 . 2 (xψxxψ)
3 19.8a 1479 . . . 4 (ψxψ)
43imim2i 12 . . 3 ((φψ) → (φxψ))
54sps 1427 . 2 (x(φψ) → (φxψ))
61, 2, 5exlimdh 1484 1 (x(φψ) → (xφxψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  eximi  1488  exbi  1492  eximdh  1499  19.29  1508  19.25  1514  alexim  1533  19.23t  1564  spimt  1621  equvini  1638  nfexd  1641  ax10oe  1675  sbcof2  1688  spsbim  1721  mor  1939  rexim  2407  elex22  2563  elex2  2564  vtoclegft  2619  spcimgft  2623  spcimegft  2625  spc2gv  2637  spc3gv  2639  ssoprab2  5503  bj-inf2vnlem1  9400
  Copyright terms: Public domain W3C validator