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 41861. 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 41861 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbi 233 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 41860 |
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 210 df-vd1 41861 |
This theorem is referenced by: vd12 41891 vd13 41892 gen11nv 41908 gen12 41909 exinst11 41917 e1a 41918 el1 41919 e223 41926 e111 41965 e1111 41966 el2122old 42010 el12 42017 el123 42055 un0.1 42070 trsspwALT 42109 sspwtr 42112 pwtrVD 42115 pwtrrVD 42116 snssiALTVD 42118 snsslVD 42120 snelpwrVD 42122 unipwrVD 42123 sstrALT2VD 42125 suctrALT2VD 42127 elex2VD 42129 elex22VD 42130 eqsbc3rVD 42131 zfregs2VD 42132 tpid3gVD 42133 en3lplem1VD 42134 en3lplem2VD 42135 en3lpVD 42136 3ornot23VD 42138 orbi1rVD 42139 3orbi123VD 42141 sbc3orgVD 42142 19.21a3con13vVD 42143 exbirVD 42144 exbiriVD 42145 rspsbc2VD 42146 3impexpVD 42147 3impexpbicomVD 42148 sbcoreleleqVD 42150 tratrbVD 42152 al2imVD 42153 syl5impVD 42154 ssralv2VD 42157 ordelordALTVD 42158 equncomVD 42159 imbi12VD 42164 imbi13VD 42165 sbcim2gVD 42166 sbcbiVD 42167 trsbcVD 42168 truniALTVD 42169 trintALTVD 42171 undif3VD 42173 sbcssgVD 42174 csbingVD 42175 simplbi2comtVD 42179 onfrALTVD 42182 csbeq2gVD 42183 csbsngVD 42184 csbxpgVD 42185 csbresgVD 42186 csbrngVD 42187 csbima12gALTVD 42188 csbunigVD 42189 csbfv12gALTVD 42190 con5VD 42191 relopabVD 42192 19.41rgVD 42193 2pm13.193VD 42194 hbimpgVD 42195 hbalgVD 42196 hbexgVD 42197 ax6e2eqVD 42198 ax6e2ndVD 42199 ax6e2ndeqVD 42200 2sb5ndVD 42201 2uasbanhVD 42202 e2ebindVD 42203 sb5ALTVD 42204 vk15.4jVD 42205 notnotrALTVD 42206 con3ALTVD 42207 sspwimpVD 42210 sspwimpcfVD 42212 suctrALTcfVD 42214 |
Copyright terms: Public domain | W3C validator |