![]() |
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 497 | . 2 ⊢ (𝜑 → 𝜒) |
3 | simpl2im.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: caovmo 7595 curry1 8040 fsuppunfi 9333 oiid 9485 cantnflt 9616 oemapvali 9628 cnfcom2lem 9645 cfeq0 10200 recmulnq 10908 addgt0sr 11048 mappsrpr 11052 isercolllem2 15559 dvdsaddre2b 16197 ndvdssub 16299 lcmfunsn 16528 imasvscafn 17427 subcidcl 17738 funcoppc 17769 clatleglb 18415 sgrpidmnd 18569 conjsubgen 19049 gagrpid 19082 gaass 19085 cntzssv 19116 cntzi 19117 efgredlemf 19531 abveq0 20328 abvmul 20331 abvtri 20332 cnpimaex 22630 restnlly 22856 fclsopni 23389 xmeteq0 23714 xmettri2 23716 metcnpi 23923 metcnpi2 23924 causs 24685 dvbssntr 25287 dgrlem 25613 dgrlb 25620 umgredgne 28145 nbgrcl 28332 wlkdlem3 28681 usgr2trlncrct 28800 wwlksonvtx 28849 wwlksnextproplem3 28905 erclwwlknsym 29063 erclwwlkntr 29064 1pthon2v 29146 cycpmco2lem3 32033 elrspunidl 32258 sseqf 33056 subgrwlk 33790 acycgrsubgr 33816 pr2el2 41915 rfovcnvf1od 42368 gneispaceel 42507 gneispacess 42509 linindslinci 46619 2arymaptfv 46827 f1sn2g 47007 |
Copyright terms: Public domain | W3C validator |