Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > e22 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e22.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) |
e22.2 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
e22.3 | ⊢ (𝜒 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
e22 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e22.1 | . 2 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
2 | e22.2 | . 2 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | |
3 | e22.3 | . . 3 ⊢ (𝜒 → (𝜃 → 𝜏)) | |
4 | 3 | a1i 11 | . 2 ⊢ (𝜒 → (𝜒 → (𝜃 → 𝜏))) |
5 | 1, 1, 2, 4 | e222 40990 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 40931 |
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 209 df-an 399 df-vd2 40932 |
This theorem is referenced by: e22an 41026 e02 41051 e12 41078 e20 41081 e21 41084 sspwtr 41175 pwtrVD 41178 pwtrrVD 41179 elex22VD 41193 tpid3gVD 41196 en3lplem2VD 41198 imbi12VD 41227 truniALTVD 41232 trintALTVD 41234 onfrALTlem3VD 41241 onfrALTlem2VD 41243 ax6e2eqVD 41261 ax6e2ndeqVD 41263 sb5ALTVD 41267 |
Copyright terms: Public domain | W3C validator |