![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > idn2 | Structured version Visualization version Unicode version |
Description: Virtual deduction identity rule which is idd 25 with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
idn2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 25 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | dfvd2ir 36998 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
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 190 df-an 377 df-vd2 36990 |
This theorem is referenced by: trsspwALT 37245 sspwtr 37248 pwtrVD 37259 pwtrrVD 37260 snssiALTVD 37262 sstrALT2VD 37269 suctrALT2VD 37271 elex2VD 37273 elex22VD 37274 eqsbc3rVD 37275 tpid3gVD 37277 en3lplem1VD 37278 en3lplem2VD 37279 3ornot23VD 37282 orbi1rVD 37283 19.21a3con13vVD 37287 exbirVD 37288 exbiriVD 37289 rspsbc2VD 37290 tratrbVD 37297 syl5impVD 37299 ssralv2VD 37302 imbi12VD 37309 imbi13VD 37310 sbcim2gVD 37311 sbcbiVD 37312 truniALTVD 37314 trintALTVD 37316 onfrALTlem3VD 37323 onfrALTlem2VD 37325 onfrALTlem1VD 37326 relopabVD 37337 19.41rgVD 37338 hbimpgVD 37340 ax6e2eqVD 37343 ax6e2ndeqVD 37345 sb5ALTVD 37349 vk15.4jVD 37350 con3ALTVD 37352 |
Copyright terms: Public domain | W3C validator |