![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr3l | 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 |
---|---|
simpr3l | ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprl 789 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr3 1247 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 |
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 1115 |
This theorem is referenced by: ax5seg 26237 axcont 26275 nosupbnd1lem5 32397 segconeq 32656 idinside 32730 btwnconn1lem10 32742 segletr 32760 cdlemc3 36268 cdlemc4 36269 cdleme1 36302 cdleme2 36303 cdleme3b 36304 cdleme3c 36305 cdleme3e 36307 cdleme27a 36442 stoweidlem56 41067 |
Copyright terms: Public domain | W3C validator |