Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simplr3 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simplr3 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr3 1062 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | adantr 480 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: soltmin 5451 frfi 8090 wemappo 8337 iccsplit 12176 ccatswrd 13308 swrdccat3 13343 pcdvdstr 15418 vdwlem12 15534 cshwsidrepswmod0 15639 iscatd2 16165 oppccomfpropd 16210 initoeu2lem0 16486 resssetc 16565 resscatc 16578 yonedalem4c 16740 mod1ile 16928 mod2ile 16929 prdsmndd 17146 grprcan 17278 mulgnn0dir 17394 mulgdir 17396 mulgass 17402 mulgnn0di 18054 mulgdi 18055 dprd2da 18264 lmodprop2d 18748 lssintcl 18785 prdslmodd 18790 islmhm2 18859 islbs2 18975 islbs3 18976 dmatmul 20122 mdetmul 20248 restopnb 20789 iuncon 21041 1stcelcls 21074 blsscls2 22119 stdbdbl 22132 xrsblre 22422 icccmplem2 22434 itg1val2 23257 cvxcl 24511 colline 25344 tglowdim2ln 25346 f1otrg 25551 f1otrge 25552 ax5seglem4 25612 ax5seglem5 25613 axcontlem3 25646 axcontlem8 25651 axcontlem9 25652 eengtrkg 25665 el2wlksotot 26409 xrofsup 28923 submomnd 29041 ogrpaddltbi 29050 erdszelem8 30434 rescon 30482 cvmliftmolem2 30518 cvmlift2lem12 30550 broutsideof3 31403 outsideoftr 31406 outsidele 31409 ltltncvr 33727 atcvrj2b 33736 cvrat4 33747 cvrat42 33748 2at0mat0 33829 islpln2a 33852 paddasslem11 34134 pmod1i 34152 lhpm0atN 34333 lautcvr 34396 cdlemg4c 34918 tendoplass 35089 tendodi1 35090 tendodi2 35091 dgrsub2 36724 ssinc 38292 ssdec 38293 ioondisj2 38561 ioondisj1 38562 pfxccat3 40289 frgr3v 41445 ply1mulgsumlem2 41969 |
Copyright terms: Public domain | W3C validator |