![]() |
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 769 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2antr2 1187 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1085 |
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 1087 |
This theorem is referenced by: poxp2 8131 poxp3 8138 frrlem8 8280 ttrcltr 9713 ttrclss 9717 rnttrcl 9719 ttrclselem2 9723 oppccatid 17669 subccatid 17800 setccatid 18038 catccatid 18060 estrccatid 18087 xpccatid 18144 kerf1ghm 19161 gsmsymgreqlem1 19339 ax5seg 28463 3pthdlem1 29684 segconeq 35286 ifscgr 35320 brofs2 35353 brifs2 35354 idinside 35360 btwnconn1lem8 35370 btwnconn1lem11 35373 btwnconn1lem12 35374 segcon2 35381 seglecgr12im 35386 unbdqndv2 35690 lplnexllnN 38738 paddasslem9 39002 paddasslem15 39008 pmodlem2 39021 lhp2lt 39175 isthincd2 47745 mndtccatid 47800 |
Copyright terms: Public domain | W3C validator |