![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > in1 | Structured version Visualization version GIF version |
Description: Inference form of df-vd1 39103. Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
in1.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
Ref | Expression |
---|---|
in1 | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | in1.1 | . 2 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | df-vd1 39103 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbi 220 | 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: vd12 39142 vd13 39143 gen11nv 39159 gen12 39160 exinst11 39168 e1a 39169 el1 39170 e223 39177 e111 39216 e1111 39217 el2122old 39261 el12 39270 el123 39308 un0.1 39323 trsspwALT 39362 sspwtr 39365 pwtrVD 39373 pwtrrVD 39374 snssiALTVD 39376 snsslVD 39378 snelpwrVD 39380 unipwrVD 39381 sstrALT2VD 39383 suctrALT2VD 39385 elex2VD 39387 elex22VD 39388 eqsbc3rVD 39389 zfregs2VD 39390 tpid3gVD 39391 en3lplem1VD 39392 en3lplem2VD 39393 en3lpVD 39394 3ornot23VD 39396 orbi1rVD 39397 3orbi123VD 39399 sbc3orgVD 39400 19.21a3con13vVD 39401 exbirVD 39402 exbiriVD 39403 rspsbc2VD 39404 3impexpVD 39405 3impexpbicomVD 39406 sbcoreleleqVD 39409 tratrbVD 39411 al2imVD 39412 syl5impVD 39413 ssralv2VD 39416 ordelordALTVD 39417 equncomVD 39418 imbi12VD 39423 imbi13VD 39424 sbcim2gVD 39425 sbcbiVD 39426 trsbcVD 39427 truniALTVD 39428 trintALTVD 39430 undif3VD 39432 sbcssgVD 39433 csbingVD 39434 simplbi2comtVD 39438 onfrALTVD 39441 csbeq2gVD 39442 csbsngVD 39443 csbxpgVD 39444 csbresgVD 39445 csbrngVD 39446 csbima12gALTVD 39447 csbunigVD 39448 csbfv12gALTVD 39449 con5VD 39450 relopabVD 39451 19.41rgVD 39452 2pm13.193VD 39453 hbimpgVD 39454 hbalgVD 39455 hbexgVD 39456 ax6e2eqVD 39457 ax6e2ndVD 39458 ax6e2ndeqVD 39459 2sb5ndVD 39460 2uasbanhVD 39461 e2ebindVD 39462 sb5ALTVD 39463 vk15.4jVD 39464 notnotrALTVD 39465 con3ALTVD 39466 sspwimpVD 39469 sspwimpcfVD 39471 suctrALTcfVD 39473 |
Copyright terms: Public domain | W3C validator |