![]() |
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 761 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr2 1197 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 1073 |
This theorem is referenced by: oppccatid 16764 subccatid 16891 setccatid 17119 catccatid 17137 estrccatid 17157 xpccatid 17214 gsmsymgreqlem1 18233 kerf1ghm 19134 kerf1hrmOLD 19135 nllyidm 21701 ax5seg 26287 3pthdlem1 27581 segconeq 32720 ifscgr 32754 brofs2 32787 brifs2 32788 idinside 32794 btwnconn1lem8 32804 btwnconn1lem12 32808 segcon2 32815 segletr 32824 outsidele 32842 unbdqndv2 33098 lplnexllnN 35712 paddasslem9 35976 pmodlem2 35995 lhp2lt 36149 cdlemc3 36341 cdlemc4 36342 cdlemd1 36346 cdleme3b 36377 cdleme3c 36378 cdleme42ke 36633 cdlemg4c 36760 |
Copyright terms: Public domain | W3C validator |