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 1078 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | 1 | adantl 481 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: oppccatid 16202 subccatid 16329 setccatid 16557 catccatid 16575 estrccatid 16595 xpccatid 16651 gsmsymgreqlem1 17673 dmdprdsplit 18269 neiptopnei 20746 neitr 20794 neitx 21220 tx1stc 21263 utop3cls 21865 metustsym 22170 ax5seg 25618 frgrawopreg 26576 esumpcvgval 29467 esum2d 29482 ifscgr 31321 brofs2 31354 brifs2 31355 btwnconn1lem8 31371 btwnconn1lem12 31375 seglecgr12im 31387 unbdqndv2 31672 lhp2lt 34305 cdlemd1 34503 cdleme3b 34534 cdleme3c 34535 cdleme3e 34537 cdlemf2 34868 cdlemg4c 34918 cdlemn11pre 35517 dihmeetlem12N 35625 stoweidlem60 38953 3pthdlem1 41331 frgrwopreg 41486 |
Copyright terms: Public domain | W3C validator |