![]() |
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 772 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2antr1 1189 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: poxp2 8076 oppccatid 17606 subccatid 17737 setccatid 17975 catccatid 17997 estrccatid 18024 xpccatid 18081 gsmsymgreqlem1 19217 dmdprdsplit 19831 neitr 22547 neitx 22974 tx1stc 23017 utop3cls 23619 metustsym 23927 clwwlkccat 28976 3pthdlem1 29150 archiabllem1 32078 esumpcvgval 32734 esum2d 32749 ifscgr 34675 btwnconn1lem8 34725 btwnconn1lem11 34728 btwnconn1lem12 34729 segletr 34745 broutsideof3 34757 unbdqndv2 35020 lhp2lt 38510 cdlemf2 39071 cdlemn11pre 39719 stoweidlem60 44387 isthincd2 47144 mndtccatid 47199 |
Copyright terms: Public domain | W3C validator |