![]() |
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 1189 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: poxp2 8074 poxp3 8081 frrlem8 8223 ttrcltr 9651 ttrclss 9655 rnttrcl 9657 ttrclselem2 9661 oppccatid 17600 subccatid 17731 setccatid 17969 catccatid 17991 estrccatid 18018 xpccatid 18075 gsmsymgreqlem1 19210 kerf1ghm 20175 ax5seg 27885 3pthdlem1 29106 segconeq 34586 ifscgr 34620 brofs2 34653 brifs2 34654 idinside 34660 btwnconn1lem8 34670 btwnconn1lem11 34673 btwnconn1lem12 34674 segcon2 34681 seglecgr12im 34686 unbdqndv2 34965 lplnexllnN 38018 paddasslem9 38282 paddasslem15 38288 pmodlem2 38301 lhp2lt 38455 isthincd2 47030 mndtccatid 47085 |
Copyright terms: Public domain | W3C validator |