![]() |
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 773 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2antr2 1188 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: poxp2 8167 poxp3 8174 frrlem8 8317 ttrcltr 9754 ttrclss 9758 rnttrcl 9760 ttrclselem2 9764 oppccatid 17766 subccatid 17897 setccatid 18138 catccatid 18160 estrccatid 18187 xpccatid 18244 kerf1ghm 19278 gsmsymgreqlem1 19463 ax5seg 28968 3pthdlem1 30193 segconeq 35992 ifscgr 36026 brofs2 36059 brifs2 36060 idinside 36066 btwnconn1lem8 36076 btwnconn1lem11 36079 btwnconn1lem12 36080 segcon2 36087 seglecgr12im 36092 unbdqndv2 36494 lplnexllnN 39547 paddasslem9 39811 paddasslem15 39817 pmodlem2 39830 lhp2lt 39984 isthincd2 48838 mndtccatid 48896 |
Copyright terms: Public domain | W3C validator |