|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > e12 | Structured version Visualization version GIF version | ||
| Description: A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| e12.1 | ⊢ ( 𝜑 ▶ 𝜓 ) | 
| e12.2 | ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) | 
| e12.3 | ⊢ (𝜓 → (𝜃 → 𝜏)) | 
| Ref | Expression | 
|---|---|
| e12 | ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | e12.1 | . . 3 ⊢ ( 𝜑 ▶ 𝜓 ) | |
| 2 | 1 | vd12 44625 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜓 ) | 
| 3 | e12.2 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) | |
| 4 | e12.3 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
| 5 | 2, 3, 4 | e22 44696 | 1 ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ( wvd1 44594 ( wvd2 44602 | 
| 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 207 df-an 396 df-vd1 44595 df-vd2 44603 | 
| This theorem is referenced by: e12an 44750 trsspwALT 44843 sspwtr 44846 pwtrVD 44849 snssiALTVD 44852 elex2VD 44863 elex22VD 44864 eqsbc2VD 44865 en3lplem1VD 44868 3ornot23VD 44872 orbi1rVD 44873 19.21a3con13vVD 44877 exbirVD 44878 tratrbVD 44886 ssralv2VD 44891 sbcim2gVD 44900 sbcbiVD 44901 relopabVD 44926 19.41rgVD 44927 ax6e2eqVD 44932 ax6e2ndeqVD 44934 vk15.4jVD 44939 con3ALTVD 44941 | 
| Copyright terms: Public domain | W3C validator |