![]() |
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.) |
Ref | Expression |
---|---|
simplr1 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 1087 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑) | |
2 | 1 | adantr 480 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: soltmin 5567 frfi 8246 wemappo 8495 iccsplit 12343 ccatswrd 13502 sqrmo 14036 pcdvdstr 15627 vdwlem12 15743 mreexexlem4d 16354 iscatd2 16389 oppccomfpropd 16434 resssetc 16789 resscatc 16802 mod1ile 17152 mod2ile 17153 prdsmndd 17370 grprcan 17502 prdsringd 18658 lmodprop2d 18973 lssintcl 19012 prdslmodd 19017 islmhm2 19086 islbs3 19203 ofco2 20305 mdetmul 20477 restopnb 21027 regsep2 21228 iunconn 21279 blsscls2 22356 met2ndci 22374 xrsblre 22661 legso 25539 colline 25589 tglowdim2ln 25591 cgrahl 25763 f1otrg 25796 f1otrge 25797 ax5seglem4 25857 ax5seglem5 25858 axcontlem4 25892 axcontlem8 25896 axcontlem9 25897 axcontlem10 25898 eengtrkg 25910 rusgrnumwwlks 26941 frgr3v 27255 submomnd 29838 ogrpaddltbi 29847 erdszelem8 31306 nosupbnd1lem5 31983 conway 32035 btwncomim 32245 btwnswapid 32249 broutsideof3 32358 outsideoftr 32361 outsidele 32364 isbasisrelowllem1 33333 isbasisrelowllem2 33334 cvrletrN 34878 ltltncvr 35027 atcvrj2b 35036 2at0mat0 35129 paddasslem11 35434 pmod1i 35452 lautcvr 35696 tendoplass 36388 tendodi1 36389 tendodi2 36390 cdlemk34 36515 mendassa 38081 3adantlr3 39514 ssinc 39578 ssdec 39579 ioondisj2 40032 ioondisj1 40033 subsubelfzo0 41661 ply1mulgsumlem2 42500 lincresunit3lem2 42594 |
Copyright terms: Public domain | W3C validator |