![]() |
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 8124 oppccatid 17661 subccatid 17792 setccatid 18030 catccatid 18052 estrccatid 18079 xpccatid 18136 gsmsymgreqlem1 19291 dmdprdsplit 19909 neitr 22666 neitx 23093 tx1stc 23136 utop3cls 23738 metustsym 24046 clwwlkccat 29223 3pthdlem1 29397 archiabllem1 32317 esumpcvgval 33014 esum2d 33029 ifscgr 34954 btwnconn1lem8 35004 btwnconn1lem11 35007 btwnconn1lem12 35008 segletr 35024 broutsideof3 35036 unbdqndv2 35325 lhp2lt 38810 cdlemf2 39371 cdlemn11pre 40019 stoweidlem60 44711 isthincd2 47560 mndtccatid 47615 |
Copyright terms: Public domain | W3C validator |