![]() |
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 41342 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 41283 |
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-an 400 df-vd2 41284 |
This theorem is referenced by: e22an 41378 e02 41403 e12 41430 e20 41433 e21 41436 sspwtr 41527 pwtrVD 41530 pwtrrVD 41531 elex22VD 41545 tpid3gVD 41548 en3lplem2VD 41550 imbi12VD 41579 truniALTVD 41584 trintALTVD 41586 onfrALTlem3VD 41593 onfrALTlem2VD 41595 ax6e2eqVD 41613 ax6e2ndeqVD 41615 sb5ALTVD 41619 |
Copyright terms: Public domain | W3C validator |