![]() |
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 8128 poxp3 8135 frrlem8 8277 ttrcltr 9710 ttrclss 9714 rnttrcl 9716 ttrclselem2 9720 oppccatid 17664 subccatid 17795 setccatid 18033 catccatid 18055 estrccatid 18082 xpccatid 18139 gsmsymgreqlem1 19297 kerf1ghm 20281 ax5seg 28193 3pthdlem1 29414 segconeq 34977 ifscgr 35011 brofs2 35044 brifs2 35045 idinside 35051 btwnconn1lem8 35061 btwnconn1lem11 35064 btwnconn1lem12 35065 segcon2 35072 seglecgr12im 35077 unbdqndv2 35382 lplnexllnN 38430 paddasslem9 38694 paddasslem15 38700 pmodlem2 38713 lhp2lt 38867 isthincd2 47648 mndtccatid 47703 |
Copyright terms: Public domain | W3C validator |