![]() |
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 44629 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 44583 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 44584 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( 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-vd2 44576 |
This theorem is referenced by: e2bi 44630 e2bir 44631 sspwtr 44819 pwtrVD 44822 pwtrrVD 44823 suctrALT2VD 44834 tpid3gVD 44840 en3lplem1VD 44841 3ornot23VD 44845 orbi1rVD 44846 19.21a3con13vVD 44850 tratrbVD 44859 syl5impVD 44861 ssralv2VD 44864 truniALTVD 44876 trintALTVD 44878 onfrALTlem3VD 44885 onfrALTlem2VD 44887 onfrALTlem1VD 44888 relopabVD 44899 19.41rgVD 44900 hbimpgVD 44902 ax6e2eqVD 44905 ax6e2ndeqVD 44907 sb5ALTVD 44911 vk15.4jVD 44912 con3ALTVD 44914 |
Copyright terms: Public domain | W3C validator |