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

Theorem alrimih 1480
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 1466 . 2 (∀𝑥𝜑 → ∀𝑥𝜓)
41, 3syl 14 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1458  ax-gen 1460
This theorem is referenced by:  albidh  1491  alrimi  1533  nfd  1534  19.21h  1568  exlimd2  1606  exlimdh  1607  eximdh  1622  nexd  1624  exbidh  1625  hbex  1647  hbnd  1666  19.12  1676  19.38  1687  ax11i  1725  equsalh  1737  nfald  1771  nfexd  1772  aev  1823  equs5or  1841  sb4or  1844  sbbidh  1856  sb6rf  1864  alrimiv  1885  eupicka  2118  2moex  2124
  Copyright terms: Public domain W3C validator