![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfvd | Structured version Visualization version GIF version |
Description: nfv 1909 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1889. (Contributed by Mario Carneiro, 6-Oct-2016.) |
Ref | Expression |
---|---|
nfvd | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1909 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | 1 | a1i 11 | 1 ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-nf 1778 |
This theorem is referenced by: cbvaldw 2328 cbvald 2400 cbvaldva 2402 cbvexdva 2403 sbiedv 2497 nfmodv 2547 nfabdw 2915 issetft 3475 vtocldOLD 3539 sbciedOLD 3820 nfunid 4915 nfopabd 5217 copsexgw 5492 nfiotadw 6504 iota2d 6537 iota2 6538 riota5f 7404 oprabidw 7450 opiota 8064 mpoxopoveq 8225 nfttrcld 9735 axrepndlem1 10617 axunndlem1 10620 fproddivf 15967 xrofsup 32619 bj-cbvaldvav 36411 bj-cbvexdvav 36412 opelopabbv 36753 brabd 36758 cbveud 36982 cbvreud 36983 fvineqsneu 37021 wl-mo2t 37173 wl-sb8eut 37176 wl-sb8eutv 37177 wl-issetft 37180 riotasv2d 38559 cdleme42b 40081 dihvalcqpre 40838 mapdheq 41331 hdmap1eq 41404 hdmapval2lem 41434 |
Copyright terms: Public domain | W3C validator |