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 38856 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 38801 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 38802 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 38793 |
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 197 df-an 386 df-vd2 38794 |
This theorem is referenced by: e2bi 38857 e2bir 38858 sspwtr 39048 pwtrVD 39059 pwtrrVD 39060 suctrALT2VD 39071 tpid3gVD 39077 en3lplem1VD 39078 3ornot23VD 39082 orbi1rVD 39083 19.21a3con13vVD 39087 tratrbVD 39097 syl5impVD 39099 ssralv2VD 39102 truniALTVD 39114 trintALTVD 39116 onfrALTlem3VD 39123 onfrALTlem2VD 39125 onfrALTlem1VD 39126 relopabVD 39137 19.41rgVD 39138 hbimpgVD 39140 ax6e2eqVD 39143 ax6e2ndeqVD 39145 sb5ALTVD 39149 vk15.4jVD 39150 con3ALTVD 39152 |
Copyright terms: Public domain | W3C validator |