![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e12 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e12.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e12.2 | ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) |
e12.3 | ⊢ (𝜓 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
e12 | ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e12.1 | . . 3 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | 1 | vd12 44598 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜓 ) |
3 | e12.2 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) | |
4 | e12.3 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
5 | 2, 3, 4 | e22 44669 | 1 ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 44567 ( wvd2 44575 |
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 207 df-an 396 df-vd1 44568 df-vd2 44576 |
This theorem is referenced by: e12an 44723 trsspwALT 44816 sspwtr 44819 pwtrVD 44822 snssiALTVD 44825 elex2VD 44836 elex22VD 44837 eqsbc2VD 44838 en3lplem1VD 44841 3ornot23VD 44845 orbi1rVD 44846 19.21a3con13vVD 44850 exbirVD 44851 tratrbVD 44859 ssralv2VD 44864 sbcim2gVD 44873 sbcbiVD 44874 relopabVD 44899 19.41rgVD 44900 ax6e2eqVD 44905 ax6e2ndeqVD 44907 vk15.4jVD 44912 con3ALTVD 44914 |
Copyright terms: Public domain | W3C validator |