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

Theorem alrimivv 1632
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1 (φψ)
Assertion
Ref Expression
alrimivv (φxyψ)
Distinct variable groups:   φ,x   φ,y
Allowed substitution hints:   ψ(x,y)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3 (φψ)
21alrimiv 1631 . 2 (φyψ)
32alrimiv 1631 1 (φxyψ)
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  ax-17 1616
This theorem is referenced by:  2ax17  1640  euind  3023  sbnfc2  3196  uniintsn  3963  eqrelkrdv  4214  nnsucelr  4428  ssfin  4470  ssopab2dv  4715  ssrel  4844  relssdv  4849  eqrelrdv  4852  eqoprrdv  4854  funun  5146  fununi  5160  funsi  5520  ovg  5601  fntxp  5804  fnpprod  5843  fundmen  6043  enpw1  6062  enmap2lem4  6066  enmap1lem4  6072  enprmaplem3  6078  fnfrec  6320
  Copyright terms: Public domain W3C validator