Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simplr1 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
Ref | Expression |
---|---|
simplr1 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antlr 727 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 df-3an 1091 |
This theorem is referenced by: soltmin 6001 frfi 8916 wemappo 9165 iccsplit 13073 ccatswrd 14233 sqrmo 14815 pcdvdstr 16429 vdwlem12 16545 mreexexlem4d 17150 iscatd2 17184 oppccomfpropd 17231 resssetc 17598 resscatc 17615 mod1ile 17999 mod2ile 18000 prdsmndd 18206 grprcan 18401 prdsringd 19630 lmodprop2d 19961 lssintcl 20001 prdslmodd 20006 islmhm2 20075 islbs3 20192 ofco2 21348 mdetmul 21520 restopnb 22072 regsep2 22273 iunconn 22325 blsscls2 23402 met2ndci 23420 xrsblre 23708 legso 26690 colline 26740 tglowdim2ln 26742 cgrahl 26918 f1otrg 26962 f1otrge 26963 ax5seglem4 27023 ax5seglem5 27024 axcontlem4 27058 axcontlem8 27062 axcontlem9 27063 axcontlem10 27064 eengtrkg 27077 rusgrnumwwlks 28058 frgr3v 28358 submomnd 31055 ogrpaddltbi 31063 erdszelem8 32873 elmrsubrn 33195 nosupbnd1lem5 33652 conway 33730 btwncomim 34052 btwnswapid 34056 broutsideof3 34165 outsideoftr 34168 outsidele 34171 isbasisrelowllem1 35263 isbasisrelowllem2 35264 cvrletrN 37024 ltltncvr 37174 atcvrj2b 37183 2at0mat0 37276 paddasslem11 37581 pmod1i 37599 lautcvr 37843 tendoplass 38534 tendodi1 38535 tendodi2 38536 cdlemk34 38661 mendassa 40722 grumnud 41577 3adantlr3 42257 ssinc 42310 ssdec 42311 ioondisj2 42706 ioondisj1 42707 subsubelfzo0 44491 ply1mulgsumlem2 45401 lincresunit3lem2 45494 catprs 45965 |
Copyright terms: Public domain | W3C validator |