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 498 | . 2 ⊢ (𝜑 → 𝜒) |
3 | simpl2im.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: caovmo 7385 curry1 7799 fsuppunfi 8853 oiid 9005 cantnflt 9135 oemapvali 9147 cnfcom2lem 9164 cfeq0 9678 recmulnq 10386 addgt0sr 10526 mappsrpr 10530 isercolllem2 15022 dvdsaddre2b 15657 ndvdssub 15760 lcmfunsn 15988 imasvscafn 16810 subcidcl 17114 funcoppc 17145 clatleglb 17736 sgrpidmnd 17916 conjsubgen 18391 gagrpid 18424 gaass 18427 cntzssv 18458 cntzi 18459 efgredlemf 18867 abveq0 19597 abvmul 19600 abvtri 19601 cnpimaex 21864 restnlly 22090 fclsopni 22623 xmeteq0 22948 xmettri2 22950 metcnpi 23154 metcnpi2 23155 causs 23901 dvbssntr 24498 dgrlem 24819 dgrlb 24826 umgredgne 26930 nbgrcl 27117 wlkdlem3 27466 usgr2trlncrct 27584 wwlksonvtx 27633 wwlksnextproplem3 27690 erclwwlknsym 27849 erclwwlkntr 27850 1pthon2v 27932 cycpmco2lem3 30770 sseqf 31650 subgrwlk 32379 acycgrsubgr 32405 pr2el2 39930 rfovcnvf1od 40370 gneispaceel 40513 gneispacess 40515 linindslinci 44523 |
Copyright terms: Public domain | W3C validator |