Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > e2 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule. syl6 34 is e2 37877 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e2.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) |
e2.2 | ⊢ (𝜒 → 𝜃) |
Ref | Expression |
---|---|
e2 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e2.1 | . . . 4 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
2 | 1 | dfvd2i 37822 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 34 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 37823 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 37814 |
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-an 385 df-vd2 37815 |
This theorem is referenced by: e2bi 37878 e2bir 37879 sspwtr 38070 pwtrVD 38081 pwtrrVD 38082 suctrALT2VD 38093 tpid3gVD 38099 en3lplem1VD 38100 3ornot23VD 38104 orbi1rVD 38105 19.21a3con13vVD 38109 tratrbVD 38119 syl5impVD 38121 ssralv2VD 38124 truniALTVD 38136 trintALTVD 38138 onfrALTlem3VD 38145 onfrALTlem2VD 38147 onfrALTlem1VD 38148 relopabVD 38159 19.41rgVD 38160 hbimpgVD 38162 ax6e2eqVD 38165 ax6e2ndeqVD 38167 sb5ALTVD 38171 vk15.4jVD 38172 con3ALTVD 38174 |
Copyright terms: Public domain | W3C validator |