![]() |
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 43480 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 43434 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 43435 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 43426 |
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 43427 |
This theorem is referenced by: e2bi 43481 e2bir 43482 sspwtr 43670 pwtrVD 43673 pwtrrVD 43674 suctrALT2VD 43685 tpid3gVD 43691 en3lplem1VD 43692 3ornot23VD 43696 orbi1rVD 43697 19.21a3con13vVD 43701 tratrbVD 43710 syl5impVD 43712 ssralv2VD 43715 truniALTVD 43727 trintALTVD 43729 onfrALTlem3VD 43736 onfrALTlem2VD 43738 onfrALTlem1VD 43739 relopabVD 43750 19.41rgVD 43751 hbimpgVD 43753 ax6e2eqVD 43756 ax6e2ndeqVD 43758 sb5ALTVD 43762 vk15.4jVD 43763 con3ALTVD 43765 |
Copyright terms: Public domain | W3C validator |