![]() |
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 1133 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antlr 725 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: soltmin 6140 frfi 9315 wemappo 9585 iccsplit 13510 ccatswrd 14671 sqrmo 15251 pcdvdstr 16873 vdwlem12 16989 mreexexlem4d 17655 iscatd2 17689 oppccomfpropd 17737 resssetc 18109 resscatc 18126 mod1ile 18513 mod2ile 18514 prdssgrpd 18721 prdsmndd 18755 grprcan 18963 prdsrngd 20155 prdsringd 20296 lmodprop2d 20896 lssintcl 20937 prdslmodd 20942 islmhm2 21012 islbs3 21132 ofco2 22441 mdetmul 22613 restopnb 23167 regsep2 23368 iunconn 23420 blsscls2 24501 met2ndci 24519 xrsblre 24815 nosupbnd1lem5 27739 conway 27826 addsass 28016 mulscom 28137 legso 28523 colline 28573 tglowdim2ln 28575 cgrahl 28751 f1otrg 28795 f1otrge 28796 ax5seglem4 28863 ax5seglem5 28864 axcontlem4 28898 axcontlem8 28902 axcontlem9 28903 axcontlem10 28904 eengtrkg 28917 rusgrnumwwlks 29905 frgr3v 30205 lmhmimasvsca 32915 submomnd 32949 ogrpaddltbi 32957 erdszelem8 35039 elmrsubrn 35361 btwncomim 35850 btwnswapid 35854 broutsideof3 35963 outsideoftr 35966 outsidele 35969 isbasisrelowllem1 37075 isbasisrelowllem2 37076 cvrletrN 38984 ltltncvr 39135 atcvrj2b 39144 2at0mat0 39237 paddasslem11 39542 pmod1i 39560 lautcvr 39804 tendoplass 40495 tendodi1 40496 tendodi2 40497 cdlemk34 40622 mendassa 42892 grumnud 43997 3adantlr3 44676 ssinc 44725 ssdec 44726 ioondisj2 45147 ioondisj1 45148 subsubelfzo0 46975 ply1mulgsumlem2 47806 lincresunit3lem2 47899 catprs 48368 |
Copyright terms: Public domain | W3C validator |