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.) |
Ref | Expression |
---|---|
simpr1r | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1r 1086 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | adantl 482 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: oppccatid 16379 subccatid 16506 setccatid 16734 catccatid 16752 estrccatid 16772 xpccatid 16828 gsmsymgreqlem1 17850 dmdprdsplit 18446 neitr 20984 neitx 21410 tx1stc 21453 utop3cls 22055 metustsym 22360 3pthdlem1 27024 archiabllem1 29747 esumpcvgval 30140 esum2d 30155 ifscgr 32151 btwnconn1lem8 32201 btwnconn1lem11 32204 btwnconn1lem12 32205 segletr 32221 broutsideof3 32233 unbdqndv2 32502 lhp2lt 35287 cdlemf2 35850 cdlemn11pre 36499 stoweidlem60 40277 |
Copyright terms: Public domain | W3C validator |