![]() |
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 761 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr1 1196 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: oppccatid 16764 subccatid 16891 setccatid 17119 catccatid 17137 estrccatid 17157 xpccatid 17214 gsmsymgreqlem1 18233 dmdprdsplit 18833 neiptopnei 21344 neitr 21392 neitx 21819 tx1stc 21862 utop3cls 22463 metustsym 22768 ax5seg 26287 3pthdlem1 27567 esumpcvgval 30738 esum2d 30753 ifscgr 32740 brofs2 32773 brifs2 32774 btwnconn1lem8 32790 btwnconn1lem12 32794 seglecgr12im 32806 unbdqndv2 33084 lhp2lt 36157 cdlemd1 36354 cdleme3b 36385 cdleme3c 36386 cdleme3e 36388 cdlemf2 36718 cdlemg4c 36768 cdlemn11pre 37366 dihmeetlem12N 37474 stoweidlem60 41208 |
Copyright terms: Public domain | W3C validator |