Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > e10 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e10.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e10.2 | ⊢ 𝜒 |
e10.3 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
e10 | ⊢ ( 𝜑 ▶ 𝜃 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e10.1 | . 2 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | e10.2 | . . 3 ⊢ 𝜒 | |
3 | 2 | vd01 38822 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) |
4 | e10.3 | . 2 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
5 | 1, 3, 4 | e11 38913 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 38785 |
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-vd1 38786 |
This theorem is referenced by: e10an 38920 en3lpVD 39080 3orbi123VD 39085 sbc3orgVD 39086 exbiriVD 39089 3impexpVD 39091 3impexpbicomVD 39092 al2imVD 39098 equncomVD 39104 trsbcVD 39113 sbcssgVD 39119 csbingVD 39120 onfrALTVD 39127 csbsngVD 39129 csbxpgVD 39130 csbresgVD 39131 csbrngVD 39132 csbima12gALTVD 39133 csbunigVD 39134 csbfv12gALTVD 39135 con5VD 39136 hbimpgVD 39140 hbalgVD 39141 hbexgVD 39142 ax6e2eqVD 39143 ax6e2ndeqVD 39145 e2ebindVD 39148 sb5ALTVD 39149 |
Copyright terms: Public domain | W3C validator |