| 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 44590 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 44590 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
| 3 | 1, 2 | mpbir 231 | 1 ⊢ ( 𝜑 ▶ 𝜓 ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ( wvd1 44589 |
| 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 44590 |
| This theorem is referenced by: idn1 44594 vd01 44617 in2 44625 int2 44626 gen11nv 44637 gen12 44638 exinst01 44645 exinst11 44646 e1a 44647 el1 44648 e111 44694 e1111 44695 un0.1 44799 un10 44808 un01 44809 sbcoreleleqVD 44879 2uasbanhVD 44931 |
| Copyright terms: Public domain | W3C validator |