![]() |
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 44584 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: ( wvd2 44575 |
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 44576 |
This theorem is referenced by: trsspwALT 44816 sspwtr 44819 pwtrVD 44822 pwtrrVD 44823 snssiALTVD 44825 sstrALT2VD 44832 suctrALT2VD 44834 elex2VD 44836 elex22VD 44837 eqsbc2VD 44838 tpid3gVD 44840 en3lplem1VD 44841 en3lplem2VD 44842 3ornot23VD 44845 orbi1rVD 44846 19.21a3con13vVD 44850 exbirVD 44851 exbiriVD 44852 rspsbc2VD 44853 tratrbVD 44859 syl5impVD 44861 ssralv2VD 44864 imbi12VD 44871 imbi13VD 44872 sbcim2gVD 44873 sbcbiVD 44874 truniALTVD 44876 trintALTVD 44878 onfrALTlem3VD 44885 onfrALTlem2VD 44887 onfrALTlem1VD 44888 relopabVD 44899 19.41rgVD 44900 hbimpgVD 44902 ax6e2eqVD 44905 ax6e2ndeqVD 44907 sb5ALTVD 44911 vk15.4jVD 44912 con3ALTVD 44914 |
Copyright terms: Public domain | W3C validator |