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

Theorem alrimih 1401
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 1387 . 2 (∀𝑥𝜑 → ∀𝑥𝜓)
41, 3syl 14 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1379  ax-gen 1381
This theorem is referenced by:  albidh  1412  alrimi  1458  nfd  1459  19.21h  1492  exlimd2  1529  exlimdh  1530  eximdh  1545  nexd  1547  exbidh  1548  hbex  1570  hbnd  1588  19.12  1598  19.38  1609  ax11i  1646  equsalh  1658  nfald  1687  nfexd  1688  aev  1737  equs5or  1755  sb4or  1758  sbbidh  1770  sb6rf  1778  alrimiv  1799  eupicka  2025  2moex  2031
  Copyright terms: Public domain W3C validator