![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr2r | 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 |
---|---|
simpr2r | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr 771 | . 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 8146 poxp3 8153 frrlem8 8297 ttrcltr 9749 ttrclss 9753 rnttrcl 9755 ttrclselem2 9759 oppccatid 17726 subccatid 17857 setccatid 18098 catccatid 18120 estrccatid 18147 xpccatid 18204 kerf1ghm 19234 gsmsymgreqlem1 19421 ax5seg 28866 3pthdlem1 30091 segconeq 35844 ifscgr 35878 brofs2 35911 brifs2 35912 idinside 35918 btwnconn1lem8 35928 btwnconn1lem11 35931 btwnconn1lem12 35932 segcon2 35939 seglecgr12im 35944 unbdqndv2 36224 lplnexllnN 39273 paddasslem9 39537 paddasslem15 39543 pmodlem2 39556 lhp2lt 39710 isthincd2 48392 mndtccatid 48447 |
Copyright terms: Public domain | W3C validator |