| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nfvd | Structured version Visualization version GIF version | ||
| Description: nfv 1914 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1894. (Contributed by Mario Carneiro, 6-Oct-2016.) |
| Ref | Expression |
|---|---|
| nfvd | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfv 1914 | . 2 ⊢ Ⅎ𝑥𝜓 | |
| 2 | 1 | a1i 11 | 1 ⊢ (𝜑 → Ⅎ𝑥𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: cbvaldw 2340 cbvald 2412 cbvaldva 2414 cbvexdva 2415 sbiedv 2509 nfmodv 2559 nfabdw 2927 cbvexeqsetf 3495 nfunid 4913 nfopabd 5211 copsexgw 5495 nfiotadw 6517 iota2d 6549 iota2 6550 riota5f 7416 oprabidw 7462 opiota 8084 mpoxopoveq 8244 nfttrcld 9750 axrepndlem1 10632 axunndlem1 10635 fproddivf 16023 xrofsup 32771 dvelimalcasei 35090 dvelimexcasei 35092 axsepg2 35096 axsepg2ALT 35097 axnulg 35106 bj-cbvaldvav 36804 bj-cbvexdvav 36805 opelopabbv 37144 brabd 37149 cbveud 37373 cbvreud 37374 fvineqsneu 37412 wl-mo2t 37576 wl-sb8eut 37579 wl-sb8eutv 37580 wl-issetft 37583 riotasv2d 38958 cdleme42b 40480 dihvalcqpre 41237 mapdheq 41730 hdmap1eq 41803 hdmapval2lem 41833 |
| Copyright terms: Public domain | W3C validator |