![]() |
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 44000. 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 44000 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbi 229 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43999 |
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 206 df-vd1 44000 |
This theorem is referenced by: vd12 44030 vd13 44031 gen11nv 44047 gen12 44048 exinst11 44056 e1a 44057 el1 44058 e223 44065 e111 44104 e1111 44105 el2122old 44149 el12 44156 el123 44194 un0.1 44209 trsspwALT 44248 sspwtr 44251 pwtrVD 44254 pwtrrVD 44255 snssiALTVD 44257 snsslVD 44259 snelpwrVD 44261 unipwrVD 44262 sstrALT2VD 44264 suctrALT2VD 44266 elex2VD 44268 elex22VD 44269 eqsbc2VD 44270 zfregs2VD 44271 tpid3gVD 44272 en3lplem1VD 44273 en3lplem2VD 44274 en3lpVD 44275 3ornot23VD 44277 orbi1rVD 44278 3orbi123VD 44280 sbc3orgVD 44281 19.21a3con13vVD 44282 exbirVD 44283 exbiriVD 44284 rspsbc2VD 44285 3impexpVD 44286 3impexpbicomVD 44287 sbcoreleleqVD 44289 tratrbVD 44291 al2imVD 44292 syl5impVD 44293 ssralv2VD 44296 ordelordALTVD 44297 equncomVD 44298 imbi12VD 44303 imbi13VD 44304 sbcim2gVD 44305 sbcbiVD 44306 trsbcVD 44307 truniALTVD 44308 trintALTVD 44310 undif3VD 44312 sbcssgVD 44313 csbingVD 44314 simplbi2comtVD 44318 onfrALTVD 44321 csbeq2gVD 44322 csbsngVD 44323 csbxpgVD 44324 csbresgVD 44325 csbrngVD 44326 csbima12gALTVD 44327 csbunigVD 44328 csbfv12gALTVD 44329 con5VD 44330 relopabVD 44331 19.41rgVD 44332 2pm13.193VD 44333 hbimpgVD 44334 hbalgVD 44335 hbexgVD 44336 ax6e2eqVD 44337 ax6e2ndVD 44338 ax6e2ndeqVD 44339 2sb5ndVD 44340 2uasbanhVD 44341 e2ebindVD 44342 sb5ALTVD 44343 vk15.4jVD 44344 notnotrALTVD 44345 con3ALTVD 44346 sspwimpVD 44349 sspwimpcfVD 44351 suctrALTcfVD 44353 |
Copyright terms: Public domain | W3C validator |