![]() |
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 769 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr2 1186 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 1086 |
This theorem is referenced by: poxp2 8148 ttrcltr 9741 ttrclss 9745 dmttrcl 9746 ttrclselem2 9751 oppccatid 17704 subccatid 17835 setccatid 18076 catccatid 18098 estrccatid 18125 xpccatid 18182 kerf1ghm 19210 gsmsymgreqlem1 19397 nllyidm 23437 noinfbnd1lem5 27706 ax5seg 28821 3pthdlem1 30046 segconeq 35737 ifscgr 35771 brofs2 35804 brifs2 35805 idinside 35811 btwnconn1lem8 35821 btwnconn1lem12 35825 segcon2 35832 segletr 35841 outsidele 35859 unbdqndv2 36117 lplnexllnN 39167 paddasslem9 39431 pmodlem2 39450 lhp2lt 39604 cdlemc3 39796 cdlemc4 39797 cdlemd1 39801 cdleme3b 39832 cdleme3c 39833 cdleme42ke 40088 cdlemg4c 40215 isthincd2 48230 mndtccatid 48285 |
Copyright terms: Public domain | W3C validator |