|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > e1a | Structured version Visualization version GIF version | ||
| Description: A Virtual deduction elimination rule. syl 17 is e1a 44652 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| e1a.1 | ⊢ ( 𝜑 ▶ 𝜓 ) | 
| e1a.2 | ⊢ (𝜓 → 𝜒) | 
| Ref | Expression | 
|---|---|
| e1a | ⊢ ( 𝜑 ▶ 𝜒 ) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | e1a.1 | . . . 4 ⊢ ( 𝜑 ▶ 𝜓 ) | |
| 2 | 1 | in1 44596 | . . 3 ⊢ (𝜑 → 𝜓) | 
| 3 | e1a.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
| 4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → 𝜒) | 
| 5 | 4 | dfvd1ir 44598 | 1 ⊢ ( 𝜑 ▶ 𝜒 ) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ( wvd1 44594 | 
| 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-vd1 44595 | 
| This theorem is referenced by: e1bi 44654 e1bir 44655 snelpwrVD 44856 unipwrVD 44857 sstrALT2VD 44859 elex2VD 44863 elex22VD 44864 eqsbc2VD 44865 zfregs2VD 44866 tpid3gVD 44867 en3lplem1VD 44868 en3lpVD 44870 3ornot23VD 44872 3orbi123VD 44875 sbc3orgVD 44876 exbirVD 44878 3impexpVD 44881 3impexpbicomVD 44882 tratrbVD 44886 al2imVD 44887 syl5impVD 44888 ssralv2VD 44891 ordelordALTVD 44892 sbcim2gVD 44900 trsbcVD 44902 truniALTVD 44903 trintALTVD 44905 undif3VD 44907 sbcssgVD 44908 csbingVD 44909 onfrALTlem3VD 44912 simplbi2comtVD 44913 onfrALTlem2VD 44914 onfrALTVD 44916 csbeq2gVD 44917 csbsngVD 44918 csbxpgVD 44919 csbresgVD 44920 csbrngVD 44921 csbima12gALTVD 44922 csbunigVD 44923 csbfv12gALTVD 44924 con5VD 44925 relopabVD 44926 19.41rgVD 44927 2pm13.193VD 44928 hbimpgVD 44929 hbalgVD 44930 hbexgVD 44931 ax6e2eqVD 44932 ax6e2ndVD 44933 ax6e2ndeqVD 44934 2sb5ndVD 44935 2uasbanhVD 44936 e2ebindVD 44937 sb5ALTVD 44938 vk15.4jVD 44939 notnotrALTVD 44940 con3ALTVD 44941 | 
| Copyright terms: Public domain | W3C validator |