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 1190 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: oppccatid 17223 subccatid 17352 setccatid 17590 catccatid 17612 estrccatid 17639 xpccatid 17695 gsmsymgreqlem1 18822 dmdprdsplit 19434 neitr 22077 neitx 22504 tx1stc 22547 utop3cls 23149 metustsym 23453 clwwlkccat 28073 3pthdlem1 28247 archiabllem1 31166 esumpcvgval 31758 esum2d 31773 poxp2 33527 ifscgr 34083 btwnconn1lem8 34133 btwnconn1lem11 34136 btwnconn1lem12 34137 segletr 34153 broutsideof3 34165 unbdqndv2 34428 lhp2lt 37752 cdlemf2 38313 cdlemn11pre 38961 stoweidlem60 43276 isthincd2 45992 mndtccatid 46045 |
Copyright terms: Public domain | W3C validator |