![]() |
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 43387 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 43328 |
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 397 df-vd2 43329 |
This theorem is referenced by: e22an 43423 e02 43448 e12 43475 e20 43478 e21 43481 sspwtr 43572 pwtrVD 43575 pwtrrVD 43576 elex22VD 43590 tpid3gVD 43593 en3lplem2VD 43595 imbi12VD 43624 truniALTVD 43629 trintALTVD 43631 onfrALTlem3VD 43638 onfrALTlem2VD 43640 ax6e2eqVD 43658 ax6e2ndeqVD 43660 sb5ALTVD 43664 |
Copyright terms: Public domain | W3C validator |