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

Theorem alrimih 1428
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 (𝜑 → ∀𝑥𝜑)
alrimih.2 (𝜑𝜓)
Assertion
Ref Expression
alrimih (𝜑 → ∀𝑥𝜓)

Proof of Theorem alrimih
StepHypRef Expression
1 alrimih.1 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimih.2 . . 3 (𝜑𝜓)
32alimi 1414 . 2 (∀𝑥𝜑 → ∀𝑥𝜓)
41, 3syl 14 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1312
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1406  ax-gen 1408
This theorem is referenced by:  albidh  1439  alrimi  1485  nfd  1486  19.21h  1519  exlimd2  1557  exlimdh  1558  eximdh  1573  nexd  1575  exbidh  1576  hbex  1598  hbnd  1616  19.12  1626  19.38  1637  ax11i  1675  equsalh  1687  nfald  1716  nfexd  1717  aev  1766  equs5or  1784  sb4or  1787  sbbidh  1799  sb6rf  1807  alrimiv  1828  eupicka  2055  2moex  2061
  Copyright terms: Public domain W3C validator