|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simpr2r | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) | 
| Ref | Expression | 
|---|---|
| simpr2r | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simprr 773 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2antr2 1190 | 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: poxp2 8168 poxp3 8175 frrlem8 8318 ttrcltr 9756 ttrclss 9760 rnttrcl 9762 ttrclselem2 9766 oppccatid 17762 subccatid 17891 setccatid 18129 catccatid 18151 estrccatid 18176 xpccatid 18233 kerf1ghm 19265 gsmsymgreqlem1 19448 ax5seg 28953 3pthdlem1 30183 segconeq 36011 ifscgr 36045 brofs2 36078 brifs2 36079 idinside 36085 btwnconn1lem8 36095 btwnconn1lem11 36098 btwnconn1lem12 36099 segcon2 36106 seglecgr12im 36111 unbdqndv2 36512 lplnexllnN 39566 paddasslem9 39830 paddasslem15 39836 pmodlem2 39849 lhp2lt 40003 isthincd2 49086 mndtccatid 49184 | 
| Copyright terms: Public domain | W3C validator |