| 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 495 | . 2 ⊢ (𝜑 → 𝜒) |
| 3 | simpl2im.2 | . 2 ⊢ (𝜒 → 𝜃) | |
| 4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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-an 396 |
| This theorem is referenced by: caovmo 7670 curry1 8129 fsuppunfi 9428 oiid 9581 cantnflt 9712 oemapvali 9724 cnfcom2lem 9741 cfeq0 10296 recmulnq 11004 addgt0sr 11144 mappsrpr 11148 isercolllem2 15702 dvdsaddre2b 16344 ndvdssub 16446 lcmfunsn 16681 imasvscafn 17582 subcidcl 17889 funcoppc 17920 clatleglb 18563 sgrpidmnd 18752 conjsubgen 19269 gagrpid 19312 gaass 19315 cntzssv 19346 cntzi 19347 efgredlemf 19759 abveq0 20819 abvmul 20822 abvtri 20823 cnpimaex 23264 restnlly 23490 fclsopni 24023 xmeteq0 24348 xmettri2 24350 metcnpi 24557 metcnpi2 24558 causs 25332 dvbssntr 25935 dgrlem 26268 dgrlb 26275 precsexlem11 28241 umgredgne 29162 nbgrcl 29352 wlkdlem3 29702 usgr2trlncrct 29826 wwlksonvtx 29875 wwlksnextproplem3 29931 erclwwlknsym 30089 erclwwlkntr 30090 1pthon2v 30172 cycpmco2lem3 33148 idomsubr 33311 elrspunidl 33456 sseqf 34394 subgrwlk 35137 acycgrsubgr 35163 fvineqsneu 37412 pr2el2 43564 rfovcnvf1od 44017 gneispaceel 44156 gneispacess 44158 clnbgrcl 47808 linindslinci 48365 2arymaptfv 48572 f1sn2g 48760 |
| Copyright terms: Public domain | W3C validator |