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

Theorem alrimih 1374
 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 1360 . 2 (∀𝑥𝜑 → ∀𝑥𝜓)
41, 3syl 14 1 (𝜑 → ∀𝑥𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1257 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1352  ax-gen 1354 This theorem is referenced by:  albidh  1385  alrimi  1431  nfd  1432  19.21h  1465  exlimd2  1502  exlimdh  1503  eximdh  1518  nexd  1520  exbidh  1521  hbex  1543  hbnd  1561  19.12  1571  19.38  1582  ax11i  1618  equsalh  1630  nfald  1659  nfexd  1660  aev  1709  equs5or  1727  sb4or  1730  sbbid  1742  sb6rf  1749  alrimiv  1770  eupicka  1996  2moex  2002
 Copyright terms: Public domain W3C validator