![]() |
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 43330 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 43271 |
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 206 df-an 398 df-vd2 43272 |
This theorem is referenced by: e22an 43366 e02 43391 e12 43418 e20 43421 e21 43424 sspwtr 43515 pwtrVD 43518 pwtrrVD 43519 elex22VD 43533 tpid3gVD 43536 en3lplem2VD 43538 imbi12VD 43567 truniALTVD 43572 trintALTVD 43574 onfrALTlem3VD 43581 onfrALTlem2VD 43583 ax6e2eqVD 43601 ax6e2ndeqVD 43603 sb5ALTVD 43607 |
Copyright terms: Public domain | W3C validator |