| 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 727 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: soltmin 6156 frfi 9321 wemappo 9589 iccsplit 13525 ccatswrd 14706 pcdvdstr 16914 vdwlem12 17030 iscatd2 17724 oppccomfpropd 17770 resssetc 18137 resscatc 18154 mod1ile 18538 mod2ile 18539 prdssgrpd 18746 prdsmndd 18783 grprcan 18991 mulgnn0dir 19122 mulgnn0di 19843 mulgdi 19844 lmodprop2d 20922 lssintcl 20962 prdslmodd 20967 islmhm2 21037 islbs3 21157 mdetmul 22629 restopnb 23183 nrmsep 23365 iunconn 23436 ptpjopn 23620 blsscls2 24517 xrsblre 24833 icccmplem2 24845 icccvx 24981 conway 27844 addsass 28038 mulscom 28165 colline 28657 tglowdim2ln 28659 f1otrg 28879 f1otrge 28880 ax5seglem5 28948 axcontlem3 28981 axcontlem4 28982 axcontlem8 28986 eengtrkg 29001 2pthon3v 29963 erclwwlktr 30041 erclwwlkntr 30090 eucrctshift 30262 frgr3v 30294 frgr2wwlkeqm 30350 xrofsup 32771 lmhmimasvsca 33044 submomnd 33087 ogrpaddltbi 33095 erdszelem8 35203 cvmliftmolem2 35287 cvmlift2lem12 35319 r1peuqusdeg1 35648 btwnswapid 36018 btwnsegle 36118 broutsideof3 36127 outsidele 36133 isbasisrelowllem2 37357 cvrletrN 39274 ltltncvr 39425 atcvrj2b 39434 cvrat4 39445 2at0mat0 39527 islpln2a 39550 paddasslem11 39832 pmod1i 39850 lautcvr 40094 cdlemg4c 40614 tendoplass 40785 tendodi1 40786 tendodi2 40787 mendlmod 43201 mendassa 43202 3adantlr3 45045 ssinc 45092 ssdec 45093 ioondisj2 45506 ioondisj1 45507 stoweidlem60 46075 ply1mulgsumlem2 48304 lincresunit3lem2 48397 catprs 48900 oppcthinco 49088 oppcthinendcALT 49090 |
| Copyright terms: Public domain | W3C validator |