![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr2l | 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 |
---|---|
simpr2l | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprl 771 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr2 1188 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: poxp2 8167 ttrcltr 9754 ttrclss 9758 dmttrcl 9759 ttrclselem2 9764 oppccatid 17766 subccatid 17897 setccatid 18138 catccatid 18160 estrccatid 18187 xpccatid 18244 kerf1ghm 19278 gsmsymgreqlem1 19463 nllyidm 23513 noinfbnd1lem5 27787 ax5seg 28968 3pthdlem1 30193 segconeq 35992 ifscgr 36026 brofs2 36059 brifs2 36060 idinside 36066 btwnconn1lem8 36076 btwnconn1lem12 36080 segcon2 36087 segletr 36096 outsidele 36114 unbdqndv2 36494 lplnexllnN 39547 paddasslem9 39811 pmodlem2 39830 lhp2lt 39984 cdlemc3 40176 cdlemc4 40177 cdlemd1 40181 cdleme3b 40212 cdleme3c 40213 cdleme42ke 40468 cdlemg4c 40595 clnbgrgrimlem 47839 isthincd2 48838 mndtccatid 48896 |
Copyright terms: Public domain | W3C validator |