![]() |
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 767 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr1 1186 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1085 |
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 206 df-an 395 df-3an 1087 |
This theorem is referenced by: poxp2 8131 poxp3 8138 oppccatid 17669 subccatid 17800 setccatid 18038 catccatid 18060 estrccatid 18087 xpccatid 18144 gsmsymgreqlem1 19339 dmdprdsplit 19958 neiptopnei 22856 neitr 22904 neitx 23331 tx1stc 23374 utop3cls 23976 metustsym 24284 ax5seg 28463 clwwlkccat 29510 3pthdlem1 29684 esumpcvgval 33374 esum2d 33389 ifscgr 35320 brofs2 35353 brifs2 35354 btwnconn1lem8 35370 btwnconn1lem12 35374 seglecgr12im 35386 unbdqndv2 35690 lhp2lt 39175 cdlemd1 39372 cdleme3b 39403 cdleme3c 39404 cdleme3e 39406 cdlemf2 39736 cdlemg4c 39786 cdlemn11pre 40384 dihmeetlem12N 40492 stoweidlem60 45074 isthincd2 47745 mndtccatid 47800 |
Copyright terms: Public domain | W3C validator |