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 1085 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant3 1084 | 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: ps-2c 34814 cdlema1N 35077 trlval3 35474 cdleme12 35558 cdlemednpq 35586 cdleme19d 35594 cdleme19e 35595 cdleme20f 35602 cdleme20h 35604 cdleme20l2 35609 cdleme20l 35610 cdleme20m 35611 cdleme21j 35624 cdleme22a 35628 cdleme22cN 35630 cdleme22f2 35635 cdleme32b 35730 cdlemg12f 35936 cdlemg12g 35937 cdlemg12 35938 cdlemg28a 35981 cdlemg31b0N 35982 cdlemg29 35993 cdlemg33a 35994 cdlemg36 36002 cdlemg42 36017 cdlemk16a 36144 cdlemk21-2N 36179 cdlemk32 36185 cdlemkid2 36212 cdlemk54 36246 cdlemk55a 36247 dihord10 36512 |
Copyright terms: Public domain | W3C validator |