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 37807. 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 37807 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbi 219 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 37806 |
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 196 df-vd1 37807 |
This theorem is referenced by: vd12 37846 vd13 37847 gen11nv 37863 gen12 37864 exinst11 37872 e1a 37873 el1 37874 e223 37881 e111 37920 e1111 37921 el2122old 37965 el12 37974 el123 38012 un0.1 38027 trsspwALT 38067 sspwtr 38070 pwtrVD 38081 pwtrrVD 38082 snssiALTVD 38084 snsslVD 38086 snelpwrVD 38088 unipwrVD 38089 sstrALT2VD 38091 suctrALT2VD 38093 elex2VD 38095 elex22VD 38096 eqsbc3rVD 38097 zfregs2VD 38098 tpid3gVD 38099 en3lplem1VD 38100 en3lplem2VD 38101 en3lpVD 38102 3ornot23VD 38104 orbi1rVD 38105 3orbi123VD 38107 sbc3orgVD 38108 19.21a3con13vVD 38109 exbirVD 38110 exbiriVD 38111 rspsbc2VD 38112 3impexpVD 38113 3impexpbicomVD 38114 sbcoreleleqVD 38117 tratrbVD 38119 al2imVD 38120 syl5impVD 38121 ssralv2VD 38124 ordelordALTVD 38125 equncomVD 38126 imbi12VD 38131 imbi13VD 38132 sbcim2gVD 38133 sbcbiVD 38134 trsbcVD 38135 truniALTVD 38136 trintALTVD 38138 undif3VD 38140 sbcssgVD 38141 csbingVD 38142 simplbi2comtVD 38146 onfrALTVD 38149 csbeq2gVD 38150 csbsngVD 38151 csbxpgVD 38152 csbresgVD 38153 csbrngVD 38154 csbima12gALTVD 38155 csbunigVD 38156 csbfv12gALTVD 38157 con5VD 38158 relopabVD 38159 19.41rgVD 38160 2pm13.193VD 38161 hbimpgVD 38162 hbalgVD 38163 hbexgVD 38164 ax6e2eqVD 38165 ax6e2ndVD 38166 ax6e2ndeqVD 38167 2sb5ndVD 38168 2uasbanhVD 38169 e2ebindVD 38170 sb5ALTVD 38171 vk15.4jVD 38172 notnotrALTVD 38173 con3ALTVD 38174 sspwimpVD 38177 sspwimpcfVD 38179 suctrALTcfVD 38181 |
Copyright terms: Public domain | W3C validator |