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 41789 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 41743 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 41744 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 41735 |
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 210 df-an 400 df-vd2 41736 |
This theorem is referenced by: e2bi 41790 e2bir 41791 sspwtr 41979 pwtrVD 41982 pwtrrVD 41983 suctrALT2VD 41994 tpid3gVD 42000 en3lplem1VD 42001 3ornot23VD 42005 orbi1rVD 42006 19.21a3con13vVD 42010 tratrbVD 42019 syl5impVD 42021 ssralv2VD 42024 truniALTVD 42036 trintALTVD 42038 onfrALTlem3VD 42045 onfrALTlem2VD 42047 onfrALTlem1VD 42048 relopabVD 42059 19.41rgVD 42060 hbimpgVD 42062 ax6e2eqVD 42065 ax6e2ndeqVD 42067 sb5ALTVD 42071 vk15.4jVD 42072 con3ALTVD 42074 |
Copyright terms: Public domain | W3C validator |