![]() |
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 44568 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 44568 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbir 231 | 1 ⊢ ( 𝜑 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 44567 |
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 207 df-vd1 44568 |
This theorem is referenced by: idn1 44572 vd01 44595 in2 44603 int2 44604 gen11nv 44615 gen12 44616 exinst01 44623 exinst11 44624 e1a 44625 el1 44626 e111 44672 e1111 44673 un0.1 44777 un10 44786 un01 44787 sbcoreleleqVD 44857 2uasbanhVD 44909 |
Copyright terms: Public domain | W3C validator |