Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpr1l | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpr1l | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1l 1085 | . 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 neiptopnei 20936 neitr 20984 neitx 21410 tx1stc 21453 utop3cls 22055 metustsym 22360 ax5seg 25818 3pthdlem1 27024 esumpcvgval 30140 esum2d 30155 ifscgr 32151 brofs2 32184 brifs2 32185 btwnconn1lem8 32201 btwnconn1lem12 32205 seglecgr12im 32217 unbdqndv2 32502 lhp2lt 35287 cdlemd1 35485 cdleme3b 35516 cdleme3c 35517 cdleme3e 35519 cdlemf2 35850 cdlemg4c 35900 cdlemn11pre 36499 dihmeetlem12N 36607 stoweidlem60 40277 |
Copyright terms: Public domain | W3C validator |