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

Theorem alrimih 1355
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 1341 . 2 (xφxψ)
41, 3syl 14 1 (φxψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1333  ax-gen 1335
This theorem is referenced by:  albidh  1366  alrimi  1412  nfd  1413  19.21h  1446  exlimd2  1483  exlimdh  1484  eximdh  1499  nexd  1501  exbidh  1502  hbex  1524  hbnd  1542  19.12  1552  19.38  1563  ax11i  1599  equsalh  1611  nfald  1640  nfexd  1641  aev  1690  equs5or  1708  sb4or  1711  sbbid  1723  sb6rf  1730  alrimiv  1751  eupicka  1977  2moex  1983
  Copyright terms: Public domain W3C validator