![]() |
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 499 | . 2 ⊢ (𝜑 → 𝜒) |
3 | simpl2im.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: caovmo 7365 curry1 7782 fsuppunfi 8837 oiid 8989 cantnflt 9119 oemapvali 9131 cnfcom2lem 9148 cfeq0 9667 recmulnq 10375 addgt0sr 10515 mappsrpr 10519 isercolllem2 15014 dvdsaddre2b 15649 ndvdssub 15750 lcmfunsn 15978 imasvscafn 16802 subcidcl 17106 funcoppc 17137 clatleglb 17728 sgrpidmnd 17908 conjsubgen 18383 gagrpid 18416 gaass 18419 cntzssv 18450 cntzi 18451 efgredlemf 18859 abveq0 19590 abvmul 19593 abvtri 19594 cnpimaex 21861 restnlly 22087 fclsopni 22620 xmeteq0 22945 xmettri2 22947 metcnpi 23151 metcnpi2 23152 causs 23902 dvbssntr 24503 dgrlem 24826 dgrlb 24833 umgredgne 26938 nbgrcl 27125 wlkdlem3 27474 usgr2trlncrct 27592 wwlksonvtx 27641 wwlksnextproplem3 27697 erclwwlknsym 27855 erclwwlkntr 27856 1pthon2v 27938 cycpmco2lem3 30820 elrspunidl 31014 sseqf 31760 subgrwlk 32492 acycgrsubgr 32518 pr2el2 40250 rfovcnvf1od 40705 gneispaceel 40846 gneispacess 40848 linindslinci 44857 2arymaptfv 45065 |
Copyright terms: Public domain | W3C validator |