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 38802 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: ( wvd2 38793 |
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-an 386 df-vd2 38794 |
This theorem is referenced by: trsspwALT 39045 sspwtr 39048 pwtrVD 39059 pwtrrVD 39060 snssiALTVD 39062 sstrALT2VD 39069 suctrALT2VD 39071 elex2VD 39073 elex22VD 39074 eqsbc3rVD 39075 tpid3gVD 39077 en3lplem1VD 39078 en3lplem2VD 39079 3ornot23VD 39082 orbi1rVD 39083 19.21a3con13vVD 39087 exbirVD 39088 exbiriVD 39089 rspsbc2VD 39090 tratrbVD 39097 syl5impVD 39099 ssralv2VD 39102 imbi12VD 39109 imbi13VD 39110 sbcim2gVD 39111 sbcbiVD 39112 truniALTVD 39114 trintALTVD 39116 onfrALTlem3VD 39123 onfrALTlem2VD 39125 onfrALTlem1VD 39126 relopabVD 39137 19.41rgVD 39138 hbimpgVD 39140 ax6e2eqVD 39143 ax6e2ndeqVD 39145 sb5ALTVD 39149 vk15.4jVD 39150 con3ALTVD 39152 |
Copyright terms: Public domain | W3C validator |