![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > alrimivv | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (φ → ψ) |
Ref | Expression |
---|---|
alrimivv | ⊢ (φ → ∀x∀yψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (φ → ψ) | |
2 | 1 | alrimiv 1631 | . 2 ⊢ (φ → ∀yψ) |
3 | 2 | alrimiv 1631 | 1 ⊢ (φ → ∀x∀yψ) |
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 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 |