NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  alrimih Unicode version

Theorem alrimih 1565
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
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 1559 . 2
41, 3syl 15 1
Colors of variables: wff setvar class
Syntax hints:   wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1546  ax-5 1557
This theorem is referenced by:  eximdh  1588  nexdh  1589  albidh  1590  exbidh  1591  alrimiv  1631  ax11i  1647  cbvaliw  1673  alrimi  1765  hbnOLD  1777  hbimdOLD  1816  hbimOLD  1818  19.23hOLD  1820  spimehOLD  1821  equsalhwOLD  1839  19.21hOLD  1840  19.12OLD  1848  cbv3hvOLD  1851  hbnd  1883  dvelimv  1939  a16g  1945  aev  1991  a5i-o  2150  equidq  2175  aev-o  2182  ax11f  2192  eujustALT  2207
  Copyright terms: Public domain W3C validator