|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > in1 | Structured version Visualization version GIF version | ||
| Description: Inference form of df-vd1 44595. Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| in1.1 | ⊢ ( 𝜑 ▶ 𝜓 ) | 
| Ref | Expression | 
|---|---|
| in1 | ⊢ (𝜑 → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | in1.1 | . 2 ⊢ ( 𝜑 ▶ 𝜓 ) | |
| 2 | df-vd1 44595 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
| 3 | 1, 2 | mpbi 230 | 1 ⊢ (𝜑 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ( wvd1 44594 | 
| 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-vd1 44595 | 
| This theorem is referenced by: vd12 44625 vd13 44626 gen11nv 44642 gen12 44643 exinst11 44651 e1a 44652 el1 44653 e223 44660 e111 44699 e1111 44700 el2122old 44744 el12 44751 el123 44789 un0.1 44804 trsspwALT 44843 sspwtr 44846 pwtrVD 44849 pwtrrVD 44850 snssiALTVD 44852 snsslVD 44854 snelpwrVD 44856 unipwrVD 44857 sstrALT2VD 44859 suctrALT2VD 44861 elex2VD 44863 elex22VD 44864 eqsbc2VD 44865 zfregs2VD 44866 tpid3gVD 44867 en3lplem1VD 44868 en3lplem2VD 44869 en3lpVD 44870 3ornot23VD 44872 orbi1rVD 44873 3orbi123VD 44875 sbc3orgVD 44876 19.21a3con13vVD 44877 exbirVD 44878 exbiriVD 44879 rspsbc2VD 44880 3impexpVD 44881 3impexpbicomVD 44882 sbcoreleleqVD 44884 tratrbVD 44886 al2imVD 44887 syl5impVD 44888 ssralv2VD 44891 ordelordALTVD 44892 equncomVD 44893 imbi12VD 44898 imbi13VD 44899 sbcim2gVD 44900 sbcbiVD 44901 trsbcVD 44902 truniALTVD 44903 trintALTVD 44905 undif3VD 44907 sbcssgVD 44908 csbingVD 44909 simplbi2comtVD 44913 onfrALTVD 44916 csbeq2gVD 44917 csbsngVD 44918 csbxpgVD 44919 csbresgVD 44920 csbrngVD 44921 csbima12gALTVD 44922 csbunigVD 44923 csbfv12gALTVD 44924 con5VD 44925 relopabVD 44926 19.41rgVD 44927 2pm13.193VD 44928 hbimpgVD 44929 hbalgVD 44930 hbexgVD 44931 ax6e2eqVD 44932 ax6e2ndVD 44933 ax6e2ndeqVD 44934 2sb5ndVD 44935 2uasbanhVD 44936 e2ebindVD 44937 sb5ALTVD 44938 vk15.4jVD 44939 notnotrALTVD 44940 con3ALTVD 44941 sspwimpVD 44944 sspwimpcfVD 44946 suctrALTcfVD 44948 | 
| Copyright terms: Public domain | W3C validator |