![]() |
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 43435 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: ( wvd2 43426 |
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 43427 |
This theorem is referenced by: trsspwALT 43667 sspwtr 43670 pwtrVD 43673 pwtrrVD 43674 snssiALTVD 43676 sstrALT2VD 43683 suctrALT2VD 43685 elex2VD 43687 elex22VD 43688 eqsbc2VD 43689 tpid3gVD 43691 en3lplem1VD 43692 en3lplem2VD 43693 3ornot23VD 43696 orbi1rVD 43697 19.21a3con13vVD 43701 exbirVD 43702 exbiriVD 43703 rspsbc2VD 43704 tratrbVD 43710 syl5impVD 43712 ssralv2VD 43715 imbi12VD 43722 imbi13VD 43723 sbcim2gVD 43724 sbcbiVD 43725 truniALTVD 43727 trintALTVD 43729 onfrALTlem3VD 43736 onfrALTlem2VD 43738 onfrALTlem1VD 43739 relopabVD 43750 19.41rgVD 43751 hbimpgVD 43753 ax6e2eqVD 43756 ax6e2ndeqVD 43758 sb5ALTVD 43762 vk15.4jVD 43763 con3ALTVD 43765 |
Copyright terms: Public domain | W3C validator |