Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp31r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp31r | ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1r 1086 | . 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 cdlemednpq 35586 cdleme19e 35595 cdleme20h 35604 cdleme20j 35606 cdleme20l2 35609 cdleme20m 35611 cdleme22a 35628 cdleme22cN 35630 cdleme22f2 35635 cdleme26f2ALTN 35652 cdleme37m 35750 cdlemg12f 35936 cdlemg12g 35937 cdlemg12 35938 cdlemg28a 35981 cdlemg29 35993 cdlemg33a 35994 cdlemg36 36002 cdlemk16a 36144 cdlemk21-2N 36179 cdlemk54 36246 dihord10 36512 |
Copyright terms: Public domain | W3C validator |