![]() |
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 1167 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antlr 719 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∧ w3a 1108 |
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 199 df-an 386 df-3an 1110 |
This theorem is referenced by: soltmin 5749 frfi 8446 wemappo 8695 iccsplit 12556 ccatswrd 13707 sqrmo 14330 pcdvdstr 15910 vdwlem12 16026 mreexexlem4d 16619 iscatd2 16653 oppccomfpropd 16698 resssetc 17053 resscatc 17066 mod1ile 17417 mod2ile 17418 prdsmndd 17635 grprcan 17768 prdsringd 18925 lmodprop2d 19240 lssintcl 19282 prdslmodd 19287 islmhm2 19356 islbs3 19475 ofco2 20580 mdetmul 20752 restopnb 21305 regsep2 21506 iunconn 21557 blsscls2 22634 met2ndci 22652 xrsblre 22939 legso 25843 colline 25893 tglowdim2ln 25895 cgrahl 26067 f1otrg 26101 f1otrge 26102 ax5seglem4 26162 ax5seglem5 26163 axcontlem4 26197 axcontlem8 26201 axcontlem9 26202 axcontlem10 26203 eengtrkg 26215 rusgrnumwwlks 27258 rusgrnumwwlksOLD 27259 frgr3v 27617 submomnd 30219 ogrpaddltbi 30228 erdszelem8 31690 nosupbnd1lem5 32364 conway 32416 btwncomim 32626 btwnswapid 32630 broutsideof3 32739 outsideoftr 32742 outsidele 32745 isbasisrelowllem1 33694 isbasisrelowllem2 33695 cvrletrN 35287 ltltncvr 35437 atcvrj2b 35446 2at0mat0 35539 paddasslem11 35844 pmod1i 35862 lautcvr 36106 tendoplass 36797 tendodi1 36798 tendodi2 36799 cdlemk34 36924 mendassa 38538 3adantlr3 39949 ssinc 40012 ssdec 40013 ioondisj2 40451 ioondisj1 40452 subsubelfzo0 42165 ply1mulgsumlem2 42963 lincresunit3lem2 43057 |
Copyright terms: Public domain | W3C validator |