![]() |
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 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | ad2antlr 726 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: soltmin 6129 frfi 9276 wemappo 9531 iccsplit 13449 ccatswrd 14605 pcdvdstr 16796 vdwlem12 16912 iscatd2 17612 oppccomfpropd 17660 resssetc 18029 resscatc 18046 mod1ile 18433 mod2ile 18434 prdssgrpd 18611 prdsmndd 18645 grprcan 18845 mulgnn0dir 18969 mulgnn0di 19676 mulgdi 19677 lmodprop2d 20511 lssintcl 20552 prdslmodd 20557 islmhm2 20626 islbs3 20745 mdetmul 22094 restopnb 22648 nrmsep 22830 iunconn 22901 ptpjopn 23085 blsscls2 23982 xrsblre 24296 icccmplem2 24308 icccvx 24435 conway 27267 addsass 27455 mulscom 27562 colline 27867 tglowdim2ln 27869 f1otrg 28089 f1otrge 28090 ax5seglem5 28158 axcontlem3 28191 axcontlem4 28192 axcontlem8 28196 eengtrkg 28211 2pthon3v 29164 erclwwlktr 29242 erclwwlkntr 29291 eucrctshift 29463 frgr3v 29495 frgr2wwlkeqm 29551 xrofsup 31951 submomnd 32199 ogrpaddltbi 32207 erdszelem8 34120 cvmliftmolem2 34204 cvmlift2lem12 34236 btwnswapid 34920 btwnsegle 35020 broutsideof3 35029 outsidele 35035 isbasisrelowllem2 36142 cvrletrN 38049 ltltncvr 38200 atcvrj2b 38209 cvrat4 38220 2at0mat0 38302 islpln2a 38325 paddasslem11 38607 pmod1i 38625 lautcvr 38869 cdlemg4c 39389 tendoplass 39560 tendodi1 39561 tendodi2 39562 mendlmod 41806 mendassa 41807 3adantlr3 43595 ssinc 43647 ssdec 43648 ioondisj2 44079 ioondisj1 44080 stoweidlem60 44649 ply1mulgsumlem2 46908 lincresunit3lem2 47001 catprs 47471 |
Copyright terms: Public domain | W3C validator |