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 40781 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 40781 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbir 232 | 1 ⊢ ( 𝜑 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 40780 |
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 208 df-vd1 40781 |
This theorem is referenced by: idn1 40785 vd01 40808 in2 40816 int2 40817 gen11nv 40828 gen12 40829 exinst01 40836 exinst11 40837 e1a 40838 el1 40839 e111 40885 e1111 40886 un0.1 40990 un10 40999 un01 41000 sbcoreleleqVD 41070 2uasbanhVD 41122 |
Copyright terms: Public domain | W3C validator |