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 769 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr3 1186 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: ax5seg 26718 axcont 26756 nosupbnd1lem5 33207 segconeq 33466 idinside 33540 btwnconn1lem10 33552 segletr 33570 cdlemc3 37323 cdlemc4 37324 cdleme1 37357 cdleme2 37358 cdleme3b 37359 cdleme3c 37360 cdleme3e 37362 cdleme27a 37497 stoweidlem56 42335 |
Copyright terms: Public domain | W3C validator |