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

Theorem exim 1472
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 1415 . 2 (x(φψ) → xx(φψ))
2 hbe1 1365 . 2 (xψxxψ)
3 19.8a 1464 . . . 4 (ψxψ)
43imim2i 12 . . 3 ((φψ) → (φxψ))
54sps 1412 . 2 (x(φψ) → (φxψ))
61, 2, 5exlimdh 1469 1 (x(φψ) → (xφxψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226  wex 1362
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-ial 1409
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  eximi  1473  exbi  1477  eximdh  1484  19.29  1493  19.25  1499  alexim  1518  19.23t  1549  spimt  1606  equvini  1623  nfexd  1626  ax10oe  1660  sbcof2  1673  spsbim  1706  mor  1924  rexim  2391  elex22  2546  elex2  2547  vtoclegft  2602  spcimgft  2606  spcimegft  2608  spc2gv  2620  spc3gv  2622  ssoprab2  5484  bj-inf2vnlem1  7188
  Copyright terms: Public domain W3C validator