![]() |
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 8129 oppccatid 17665 subccatid 17796 setccatid 18034 catccatid 18056 estrccatid 18083 xpccatid 18140 gsmsymgreqlem1 19298 dmdprdsplit 19917 neitr 22684 neitx 23111 tx1stc 23154 utop3cls 23756 metustsym 24064 clwwlkccat 29243 3pthdlem1 29417 archiabllem1 32339 esumpcvgval 33076 esum2d 33091 ifscgr 35016 btwnconn1lem8 35066 btwnconn1lem11 35069 btwnconn1lem12 35070 segletr 35086 broutsideof3 35098 unbdqndv2 35387 lhp2lt 38872 cdlemf2 39433 cdlemn11pre 40081 stoweidlem60 44776 isthincd2 47658 mndtccatid 47713 |
Copyright terms: Public domain | W3C validator |