![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl2im | Structured version Visualization version GIF version |
Description: Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) (Proof shortened by Wolf Lammen, 26-Mar-2022.) |
Ref | Expression |
---|---|
simpl2im.1 | ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
simpl2im.2 | ⊢ (𝜒 → 𝜃) |
Ref | Expression |
---|---|
simpl2im | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2im.1 | . . 3 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | |
2 | 1 | simprd 494 | . 2 ⊢ (𝜑 → 𝜒) |
3 | simpl2im.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: caovmo 7658 curry1 8109 fsuppunfi 9413 oiid 9566 cantnflt 9697 oemapvali 9709 cnfcom2lem 9726 cfeq0 10281 recmulnq 10989 addgt0sr 11129 mappsrpr 11133 isercolllem2 15648 dvdsaddre2b 16287 ndvdssub 16389 lcmfunsn 16618 imasvscafn 17522 subcidcl 17833 funcoppc 17864 clatleglb 18513 sgrpidmnd 18702 conjsubgen 19214 gagrpid 19257 gaass 19260 cntzssv 19291 cntzi 19292 efgredlemf 19708 abveq0 20718 abvmul 20721 abvtri 20722 cnpimaex 23204 restnlly 23430 fclsopni 23963 xmeteq0 24288 xmettri2 24290 metcnpi 24497 metcnpi2 24498 causs 25270 dvbssntr 25873 dgrlem 26208 dgrlb 26215 precsexlem11 28165 umgredgne 29030 nbgrcl 29220 wlkdlem3 29570 usgr2trlncrct 29689 wwlksonvtx 29738 wwlksnextproplem3 29794 erclwwlknsym 29952 erclwwlkntr 29953 1pthon2v 30035 cycpmco2lem3 32941 idomsubr 33095 elrspunidl 33240 sseqf 34140 subgrwlk 34870 acycgrsubgr 34896 pr2el2 43120 rfovcnvf1od 43573 gneispaceel 43712 gneispacess 43714 clnbgrcl 47295 linindslinci 47699 2arymaptfv 47907 f1sn2g 48086 |
Copyright terms: Public domain | W3C validator |