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

Theorem alrimih 1338
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
Hypotheses
Ref Expression
alrimih.1 (φxφ)
alrimih.2 (φψ)
Assertion
Ref Expression
alrimih (φxψ)

Proof of Theorem alrimih
StepHypRef Expression
1 alrimih.1 . 2 (φxφ)
2 alrimih.2 . . 3 (φψ)
32alimi 1324 . 2 (xφxψ)
41, 3syl 14 1 (φxψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1316  ax-gen 1318
This theorem is referenced by:  albidh  1349  alrimi  1396  nfd  1397  19.21h  1431  exlimd2  1468  exlimdh  1469  eximdh  1484  nexd  1486  exbidh  1487  hbex  1509  hbnd  1527  19.12  1537  19.38  1548  ax11i  1584  equsalh  1596  nfald  1625  nfexd  1626  aev  1675  equs5or  1693  sb4or  1696  sbbid  1708  sb6rf  1715  alrimiv  1736  eupicka  1962  2moex  1968
  Copyright terms: Public domain W3C validator