Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp31l | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp31l | ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1l 1078 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant3 1077 | 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: ps-2c 33832 cdlema1N 34095 trlval3 34492 cdleme12 34576 cdlemednpq 34604 cdleme19d 34612 cdleme19e 34613 cdleme20f 34620 cdleme20h 34622 cdleme20l2 34627 cdleme20l 34628 cdleme20m 34629 cdleme21j 34642 cdleme22a 34646 cdleme22cN 34648 cdleme22f2 34653 cdleme32b 34748 cdlemg12f 34954 cdlemg12g 34955 cdlemg12 34956 cdlemg28a 34999 cdlemg31b0N 35000 cdlemg29 35011 cdlemg33a 35012 cdlemg36 35020 cdlemg42 35035 cdlemk16a 35162 cdlemk21-2N 35197 cdlemk32 35203 cdlemkid2 35230 cdlemk54 35264 cdlemk55a 35265 dihord10 35530 |
Copyright terms: Public domain | W3C validator |