![]() |
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 39103 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 39103 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbir 221 | 1 ⊢ ( 𝜑 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 39102 |
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 197 df-vd1 39103 |
This theorem is referenced by: idn1 39107 vd01 39139 in2 39147 int2 39148 gen11nv 39159 gen12 39160 exinst01 39167 exinst11 39168 e1a 39169 el1 39170 e111 39216 e1111 39217 un0.1 39323 un10 39332 un01 39333 2uasbanhVD 39461 |
Copyright terms: Public domain | W3C validator |