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 1128 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antlr 723 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: soltmin 5989 frfi 8751 wemappo 9001 iccsplit 12859 ccatswrd 14018 sqrmo 14599 pcdvdstr 16200 vdwlem12 16316 mreexexlem4d 16906 iscatd2 16940 oppccomfpropd 16985 resssetc 17340 resscatc 17353 mod1ile 17703 mod2ile 17704 prdsmndd 17932 grprcan 18075 prdsringd 19291 lmodprop2d 19625 lssintcl 19665 prdslmodd 19670 islmhm2 19739 islbs3 19856 ofco2 20988 mdetmul 21160 restopnb 21711 regsep2 21912 iunconn 21964 blsscls2 23041 met2ndci 23059 xrsblre 23346 legso 26312 colline 26362 tglowdim2ln 26364 cgrahl 26540 f1otrg 26584 f1otrge 26585 ax5seglem4 26645 ax5seglem5 26646 axcontlem4 26680 axcontlem8 26684 axcontlem9 26685 axcontlem10 26686 eengtrkg 26699 rusgrnumwwlks 27680 frgr3v 27981 submomnd 30638 ogrpaddltbi 30646 erdszelem8 32342 elmrsubrn 32664 nosupbnd1lem5 33109 conway 33161 btwncomim 33371 btwnswapid 33375 broutsideof3 33484 outsideoftr 33487 outsidele 33490 isbasisrelowllem1 34518 isbasisrelowllem2 34519 cvrletrN 36289 ltltncvr 36439 atcvrj2b 36448 2at0mat0 36541 paddasslem11 36846 pmod1i 36864 lautcvr 37108 tendoplass 37799 tendodi1 37800 tendodi2 37801 cdlemk34 37926 mendassa 39672 grumnud 40499 3adantlr3 41175 ssinc 41230 ssdec 41231 ioondisj2 41643 ioondisj1 41644 subsubelfzo0 43403 ply1mulgsumlem2 44369 lincresunit3lem2 44463 |
Copyright terms: Public domain | W3C validator |