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

Theorem alrimi 1765
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
alrimi.1 xφ
alrimi.2 (φψ)
Assertion
Ref Expression
alrimi (φxψ)

Proof of Theorem alrimi
StepHypRef Expression
1 alrimi.1 . . 3 xφ
21nfri 1762 . 2 (φxφ)
3 alrimi.2 . 2 (φψ)
42, 3alrimih 1565 1 (φxψ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wnf 1544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545
This theorem is referenced by:  nfd  1766  a5i  1789  exlimd  1806  19.12  1847  nfald  1852  nfaldOLD  1853  19.38OLD  1874  equs5e  1888  equsal  1960  sbbid  2078  dvelimdf  2082  sb6rf  2091  sb8  2092  nfsbd  2111  eupicka  2268  2moex  2275  abbid  2466  nfcd  2484  ralrimi  2695  ceqsalg  2883  ceqsex  2893  vtocldf  2906  morex  3020  sbciedf  3081  csbiebt  3172  csbiedf  3173  iota2df  4365  sniota  4369  ncfinlower  4483  ssopab2b  4713  imadif  5171
  Copyright terms: Public domain W3C validator