Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > e1a | Structured version Visualization version GIF version |
Description: A Virtual deduction elimination rule. syl 17 is e1a 41918 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e1a.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e1a.2 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
e1a | ⊢ ( 𝜑 ▶ 𝜒 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e1a.1 | . . . 4 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | 1 | in1 41862 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | e1a.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → 𝜒) |
5 | 4 | dfvd1ir 41864 | 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: e1bi 41920 e1bir 41921 snelpwrVD 42122 unipwrVD 42123 sstrALT2VD 42125 elex2VD 42129 elex22VD 42130 eqsbc3rVD 42131 zfregs2VD 42132 tpid3gVD 42133 en3lplem1VD 42134 en3lpVD 42136 3ornot23VD 42138 3orbi123VD 42141 sbc3orgVD 42142 exbirVD 42144 3impexpVD 42147 3impexpbicomVD 42148 tratrbVD 42152 al2imVD 42153 syl5impVD 42154 ssralv2VD 42157 ordelordALTVD 42158 sbcim2gVD 42166 trsbcVD 42168 truniALTVD 42169 trintALTVD 42171 undif3VD 42173 sbcssgVD 42174 csbingVD 42175 onfrALTlem3VD 42178 simplbi2comtVD 42179 onfrALTlem2VD 42180 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 |
Copyright terms: Public domain | W3C validator |