![]() |
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 771 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2antr1 1185 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 1086 |
This theorem is referenced by: poxp2 8148 oppccatid 17704 subccatid 17835 setccatid 18076 catccatid 18098 estrccatid 18125 xpccatid 18182 gsmsymgreqlem1 19397 dmdprdsplit 20016 neitr 23128 neitx 23555 tx1stc 23598 utop3cls 24200 metustsym 24508 clwwlkccat 29872 3pthdlem1 30046 archiabllem1 32993 esumpcvgval 33828 esum2d 33843 ifscgr 35771 btwnconn1lem8 35821 btwnconn1lem11 35824 btwnconn1lem12 35825 segletr 35841 broutsideof3 35853 unbdqndv2 36117 lhp2lt 39604 cdlemf2 40165 cdlemn11pre 40813 stoweidlem60 45586 isthincd2 48230 mndtccatid 48285 |
Copyright terms: Public domain | W3C validator |