|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simpr1l | 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 | 
|---|---|
| simpr1l | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simprl 771 | . 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 poxp3 8175 oppccatid 17762 subccatid 17891 setccatid 18129 catccatid 18151 estrccatid 18176 xpccatid 18233 gsmsymgreqlem1 19448 dmdprdsplit 20067 neiptopnei 23140 neitr 23188 neitx 23615 tx1stc 23658 utop3cls 24260 metustsym 24568 ax5seg 28953 clwwlkccat 30009 3pthdlem1 30183 esumpcvgval 34079 esum2d 34094 ifscgr 36045 brofs2 36078 brifs2 36079 btwnconn1lem8 36095 btwnconn1lem12 36099 seglecgr12im 36111 unbdqndv2 36512 lhp2lt 40003 cdlemd1 40200 cdleme3b 40231 cdleme3c 40232 cdleme3e 40234 cdlemf2 40564 cdlemg4c 40614 cdlemn11pre 41212 dihmeetlem12N 41320 stoweidlem60 46075 isthincd2 49086 mndtccatid 49184 | 
| Copyright terms: Public domain | W3C validator |