| Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > e2 | Structured version Visualization version GIF version | ||
| Description: A virtual deduction elimination rule. syl6 35 is e2 44651 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| e2.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) |
| e2.2 | ⊢ (𝜒 → 𝜃) |
| Ref | Expression |
|---|---|
| e2 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | e2.1 | . . . 4 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
| 2 | 1 | dfvd2i 44605 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
| 4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
| 5 | 4 | dfvd2ir 44606 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ( wvd2 44597 |
| 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-vd2 44598 |
| This theorem is referenced by: e2bi 44652 e2bir 44653 sspwtr 44841 pwtrVD 44844 pwtrrVD 44845 suctrALT2VD 44856 tpid3gVD 44862 en3lplem1VD 44863 3ornot23VD 44867 orbi1rVD 44868 19.21a3con13vVD 44872 tratrbVD 44881 syl5impVD 44883 ssralv2VD 44886 truniALTVD 44898 trintALTVD 44900 onfrALTlem3VD 44907 onfrALTlem2VD 44909 onfrALTlem1VD 44910 relopabVD 44921 19.41rgVD 44922 hbimpgVD 44924 ax6e2eqVD 44927 ax6e2ndeqVD 44929 sb5ALTVD 44933 vk15.4jVD 44934 con3ALTVD 44936 |
| Copyright terms: Public domain | W3C validator |