![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dfvd1ir | Structured version Visualization version GIF version |
Description: Inference form of df-vd1 42944 with the virtual deduction as the assertion. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
dfvd1ir.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
dfvd1ir | ⊢ ( 𝜑 ▶ 𝜓 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfvd1ir.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | df-vd1 42944 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbir 230 | 1 ⊢ ( 𝜑 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 42943 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-vd1 42944 |
This theorem is referenced by: idn1 42948 vd01 42971 in2 42979 int2 42980 gen11nv 42991 gen12 42992 exinst01 42999 exinst11 43000 e1a 43001 el1 43002 e111 43048 e1111 43049 un0.1 43153 un10 43162 un01 43163 sbcoreleleqVD 43233 2uasbanhVD 43285 |
Copyright terms: Public domain | W3C validator |