|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > e22 | Structured version Visualization version GIF version | ||
| Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| e22.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | 
| e22.2 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | 
| e22.3 | ⊢ (𝜒 → (𝜃 → 𝜏)) | 
| Ref | Expression | 
|---|---|
| e22 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | e22.1 | . 2 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
| 2 | e22.2 | . 2 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | |
| 3 | e22.3 | . . 3 ⊢ (𝜒 → (𝜃 → 𝜏)) | |
| 4 | 3 | a1i 11 | . 2 ⊢ (𝜒 → (𝜒 → (𝜃 → 𝜏))) | 
| 5 | 1, 1, 2, 4 | e222 44661 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ( 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-vd2 44603 | 
| This theorem is referenced by: e22an 44697 e02 44722 e12 44749 e20 44752 e21 44755 sspwtr 44846 pwtrVD 44849 pwtrrVD 44850 elex22VD 44864 tpid3gVD 44867 en3lplem2VD 44869 imbi12VD 44898 truniALTVD 44903 trintALTVD 44905 onfrALTlem3VD 44912 onfrALTlem2VD 44914 ax6e2eqVD 44932 ax6e2ndeqVD 44934 sb5ALTVD 44938 | 
| Copyright terms: Public domain | W3C validator |