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 42251 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 42205 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 42206 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 42197 |
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 42198 |
This theorem is referenced by: e2bi 42252 e2bir 42253 sspwtr 42441 pwtrVD 42444 pwtrrVD 42445 suctrALT2VD 42456 tpid3gVD 42462 en3lplem1VD 42463 3ornot23VD 42467 orbi1rVD 42468 19.21a3con13vVD 42472 tratrbVD 42481 syl5impVD 42483 ssralv2VD 42486 truniALTVD 42498 trintALTVD 42500 onfrALTlem3VD 42507 onfrALTlem2VD 42509 onfrALTlem1VD 42510 relopabVD 42521 19.41rgVD 42522 hbimpgVD 42524 ax6e2eqVD 42527 ax6e2ndeqVD 42529 sb5ALTVD 42533 vk15.4jVD 42534 con3ALTVD 42536 |
Copyright terms: Public domain | W3C validator |