![]() |
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 773 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2antr1 1187 | 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 oppccatid 17766 subccatid 17897 setccatid 18138 catccatid 18160 estrccatid 18187 xpccatid 18244 gsmsymgreqlem1 19463 dmdprdsplit 20082 neitr 23204 neitx 23631 tx1stc 23674 utop3cls 24276 metustsym 24584 clwwlkccat 30019 3pthdlem1 30193 archiabllem1 33183 esumpcvgval 34059 esum2d 34074 ifscgr 36026 btwnconn1lem8 36076 btwnconn1lem11 36079 btwnconn1lem12 36080 segletr 36096 broutsideof3 36108 unbdqndv2 36494 lhp2lt 39984 cdlemf2 40545 cdlemn11pre 41193 stoweidlem60 46016 isthincd2 48838 mndtccatid 48896 |
Copyright terms: Public domain | W3C validator |