New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  alrimih GIF 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 (φxφ)
alrimih.2 (φψ)
Assertion
Ref Expression
alrimih (φxψ)

Proof of Theorem alrimih
StepHypRef Expression
1 alrimih.1 . 2 (φxφ)
2 alrimih.2 . . 3 (φψ)
32alimi 1559 . 2 (xφxψ)
41, 3syl 15 1 (φxψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1540 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  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