![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr1r | 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 |
---|---|
simpr1r | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr 750 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2antr1 1203 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: oppccatid 16587 subccatid 16714 setccatid 16942 catccatid 16960 estrccatid 16980 xpccatid 17037 gsmsymgreqlem1 18058 dmdprdsplit 18655 neitr 21206 neitx 21632 tx1stc 21675 utop3cls 22276 metustsym 22581 clwwlkccat 27141 3pthdlem1 27345 archiabllem1 30088 esumpcvgval 30481 esum2d 30496 ifscgr 32489 btwnconn1lem8 32539 btwnconn1lem11 32542 btwnconn1lem12 32543 segletr 32559 broutsideof3 32571 unbdqndv2 32840 lhp2lt 35810 cdlemf2 36372 cdlemn11pre 37021 stoweidlem60 40795 |
Copyright terms: Public domain | W3C validator |