Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp22r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp22r | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2r 1081 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant2 1076 | 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: ax5seglem6 25614 segconeu 31288 3atlem2 33788 lplnexllnN 33868 lplncvrlvol2 33919 4atex 34380 cdleme3g 34539 cdleme3h 34540 cdleme11h 34571 cdleme20bN 34616 cdleme20c 34617 cdleme20f 34620 cdleme20g 34621 cdleme20j 34624 cdleme20l2 34627 cdleme20l 34628 cdleme21ct 34635 cdleme26e 34665 cdleme43fsv1snlem 34726 cdleme39n 34772 cdleme40m 34773 cdleme42k 34790 cdlemg6c 34926 cdlemg31d 35006 cdlemg33a 35012 cdlemg33c 35014 cdlemg33d 35015 cdlemg33e 35016 cdlemg33 35017 cdlemh 35123 cdlemk7u-2N 35194 cdlemk11u-2N 35195 cdlemk12u-2N 35196 cdlemk20-2N 35198 cdlemk28-3 35214 cdlemk33N 35215 cdlemk34 35216 cdlemk39 35222 cdlemkyyN 35268 |
Copyright terms: Public domain | W3C validator |