![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > idn2 | Structured version Visualization version GIF version |
Description: Virtual deduction identity rule which is idd 24 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 24 | . 2 ⊢ (𝜑 → (𝜓 → 𝜓)) | |
2 | 1 | dfvd2ir 43332 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: ( wvd2 43323 |
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-an 397 df-vd2 43324 |
This theorem is referenced by: trsspwALT 43564 sspwtr 43567 pwtrVD 43570 pwtrrVD 43571 snssiALTVD 43573 sstrALT2VD 43580 suctrALT2VD 43582 elex2VD 43584 elex22VD 43585 eqsbc2VD 43586 tpid3gVD 43588 en3lplem1VD 43589 en3lplem2VD 43590 3ornot23VD 43593 orbi1rVD 43594 19.21a3con13vVD 43598 exbirVD 43599 exbiriVD 43600 rspsbc2VD 43601 tratrbVD 43607 syl5impVD 43609 ssralv2VD 43612 imbi12VD 43619 imbi13VD 43620 sbcim2gVD 43621 sbcbiVD 43622 truniALTVD 43624 trintALTVD 43626 onfrALTlem3VD 43633 onfrALTlem2VD 43635 onfrALTlem1VD 43636 relopabVD 43647 19.41rgVD 43648 hbimpgVD 43650 ax6e2eqVD 43653 ax6e2ndeqVD 43655 sb5ALTVD 43659 vk15.4jVD 43660 con3ALTVD 43662 |
Copyright terms: Public domain | W3C validator |