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 767 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr2 1181 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: oppccatid 16977 subccatid 17104 setccatid 17332 catccatid 17350 estrccatid 17370 xpccatid 17426 gsmsymgreqlem1 18487 kerf1ghm 19426 kerf1hrmOLD 19427 nllyidm 22025 ax5seg 26651 3pthdlem1 27870 segconeq 33368 ifscgr 33402 brofs2 33435 brifs2 33436 idinside 33442 btwnconn1lem8 33452 btwnconn1lem12 33456 segcon2 33463 segletr 33472 outsidele 33490 unbdqndv2 33747 lplnexllnN 36580 paddasslem9 36844 pmodlem2 36863 lhp2lt 37017 cdlemc3 37209 cdlemc4 37210 cdlemd1 37214 cdleme3b 37245 cdleme3c 37246 cdleme42ke 37501 cdlemg4c 37628 |
Copyright terms: Public domain | W3C validator |