|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simpr1r | 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 | 
|---|---|
| simpr1r | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simprr 773 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2antr1 1189 | 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 oppccatid 17762 subccatid 17891 setccatid 18129 catccatid 18151 estrccatid 18176 xpccatid 18233 gsmsymgreqlem1 19448 dmdprdsplit 20067 neitr 23188 neitx 23615 tx1stc 23658 utop3cls 24260 metustsym 24568 clwwlkccat 30009 3pthdlem1 30183 archiabllem1 33200 esumpcvgval 34079 esum2d 34094 ifscgr 36045 btwnconn1lem8 36095 btwnconn1lem11 36098 btwnconn1lem12 36099 segletr 36115 broutsideof3 36127 unbdqndv2 36512 lhp2lt 40003 cdlemf2 40564 cdlemn11pre 41212 stoweidlem60 46075 isthincd2 49086 mndtccatid 49184 | 
| Copyright terms: Public domain | W3C validator |