| 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 44606 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜓 ) |
| Colors of variables: wff setvar class |
| Syntax hints: ( wvd2 44597 |
| 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 207 df-an 396 df-vd2 44598 |
| This theorem is referenced by: trsspwALT 44838 sspwtr 44841 pwtrVD 44844 pwtrrVD 44845 snssiALTVD 44847 sstrALT2VD 44854 suctrALT2VD 44856 elex2VD 44858 elex22VD 44859 eqsbc2VD 44860 tpid3gVD 44862 en3lplem1VD 44863 en3lplem2VD 44864 3ornot23VD 44867 orbi1rVD 44868 19.21a3con13vVD 44872 exbirVD 44873 exbiriVD 44874 rspsbc2VD 44875 tratrbVD 44881 syl5impVD 44883 ssralv2VD 44886 imbi12VD 44893 imbi13VD 44894 sbcim2gVD 44895 sbcbiVD 44896 truniALTVD 44898 trintALTVD 44900 onfrALTlem3VD 44907 onfrALTlem2VD 44909 onfrALTlem1VD 44910 relopabVD 44921 19.41rgVD 44922 hbimpgVD 44924 ax6e2eqVD 44927 ax6e2ndeqVD 44929 sb5ALTVD 44933 vk15.4jVD 44934 con3ALTVD 44936 |
| Copyright terms: Public domain | W3C validator |