![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simplr2 | 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 |
---|---|
simplr2 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 1135 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | ad2antlr 723 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1085 |
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 1087 |
This theorem is referenced by: soltmin 6136 frfi 9290 wemappo 9546 iccsplit 13466 ccatswrd 14622 pcdvdstr 16813 vdwlem12 16929 iscatd2 17629 oppccomfpropd 17677 resssetc 18046 resscatc 18063 mod1ile 18450 mod2ile 18451 prdssgrpd 18658 prdsmndd 18692 grprcan 18894 mulgnn0dir 19020 mulgnn0di 19734 mulgdi 19735 lmodprop2d 20678 lssintcl 20719 prdslmodd 20724 islmhm2 20793 islbs3 20913 mdetmul 22345 restopnb 22899 nrmsep 23081 iunconn 23152 ptpjopn 23336 blsscls2 24233 xrsblre 24547 icccmplem2 24559 icccvx 24695 conway 27537 addsass 27727 mulscom 27834 colline 28167 tglowdim2ln 28169 f1otrg 28389 f1otrge 28390 ax5seglem5 28458 axcontlem3 28491 axcontlem4 28492 axcontlem8 28496 eengtrkg 28511 2pthon3v 29464 erclwwlktr 29542 erclwwlkntr 29591 eucrctshift 29763 frgr3v 29795 frgr2wwlkeqm 29851 xrofsup 32247 lmhmimasvsca 32467 submomnd 32498 ogrpaddltbi 32506 erdszelem8 34487 cvmliftmolem2 34571 cvmlift2lem12 34603 btwnswapid 35293 btwnsegle 35393 broutsideof3 35402 outsidele 35408 isbasisrelowllem2 36540 cvrletrN 38446 ltltncvr 38597 atcvrj2b 38606 cvrat4 38617 2at0mat0 38699 islpln2a 38722 paddasslem11 39004 pmod1i 39022 lautcvr 39266 cdlemg4c 39786 tendoplass 39957 tendodi1 39958 tendodi2 39959 mendlmod 42237 mendassa 42238 3adantlr3 44026 ssinc 44077 ssdec 44078 ioondisj2 44504 ioondisj1 44505 stoweidlem60 45074 ply1mulgsumlem2 47155 lincresunit3lem2 47248 catprs 47718 |
Copyright terms: Public domain | W3C validator |