|   | 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.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) | 
| Ref | Expression | 
|---|---|
| simplr3 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simp3 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
| 2 | 1 | ad2antlr 727 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 | 
| 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 1088 | 
| This theorem is referenced by: soltmin 6155 frfi 9322 wemappo 9590 ttrclss 9761 ttrclselem2 9767 iccsplit 13526 ccatswrd 14707 pfxccat3 14773 modfsummods 15830 pcdvdstr 16915 vdwlem12 17031 cshwsidrepswmod0 17133 iscatd2 17725 oppccomfpropd 17771 initoeu2lem0 18059 resssetc 18138 resscatc 18155 yonedalem4c 18323 mod1ile 18539 mod2ile 18540 prdssgrpd 18747 prdsmndd 18784 grprcan 18992 mulgnn0dir 19123 mulgdir 19125 mulgass 19130 mulgnn0di 19844 mulgdi 19845 dprd2da 20063 lmodprop2d 20923 lssintcl 20963 prdslmodd 20968 islmhm2 21038 islbs2 21157 islbs3 21158 dmatmul 22504 mdetmul 22630 restopnb 23184 iunconn 23437 1stcelcls 23470 blsscls2 24518 stdbdbl 24531 xrsblre 24834 icccmplem2 24846 itg1val2 25720 cvxcl 27029 conway 27845 sleadd1 28023 addsass 28039 mulscom 28166 colline 28658 tglowdim2ln 28660 f1otrg 28880 f1otrge 28881 ax5seglem4 28948 ax5seglem5 28949 axcontlem3 28982 axcontlem8 28987 axcontlem9 28988 eengtrkg 29002 frgr3v 30295 xrofsup 32772 lmhmimasvsca 33045 submomnd 33088 ogrpaddltbi 33096 erdszelem8 35204 resconn 35252 cvmliftmolem2 35288 cvmlift2lem12 35320 r1peuqusdeg1 35649 broutsideof3 36128 outsideoftr 36131 outsidele 36134 ltltncvr 39426 atcvrj2b 39435 cvrat4 39446 cvrat42 39447 2at0mat0 39528 islpln2a 39551 paddasslem11 39833 pmod1i 39851 lhpm0atN 40032 lautcvr 40095 cdlemg4c 40615 tendoplass 40786 tendodi1 40787 tendodi2 40788 dgrsub2 43152 grumnud 44310 ssinc 45097 ssdec 45098 ioondisj2 45511 ioondisj1 45512 ply1mulgsumlem2 48309 catprs 48915 oppcthinco 49113 oppcthinendcALT 49115 | 
| Copyright terms: Public domain | W3C validator |