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 1192 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant2 1126 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: ax5seglem6 26648 frrlem10 33030 segconeu 33370 3atlem2 36502 lplnexllnN 36582 lplncvrlvol2 36633 4atex 37094 cdleme3g 37252 cdleme3h 37253 cdleme11h 37284 cdleme20bN 37328 cdleme20c 37329 cdleme20f 37332 cdleme20g 37333 cdleme20j 37336 cdleme20l2 37339 cdleme20l 37340 cdleme21ct 37347 cdleme26e 37377 cdleme43fsv1snlem 37438 cdleme39n 37484 cdleme40m 37485 cdleme42k 37502 cdlemg6c 37638 cdlemg31d 37718 cdlemg33a 37724 cdlemg33c 37726 cdlemg33d 37727 cdlemg33e 37728 cdlemg33 37729 cdlemh 37835 cdlemk7u-2N 37906 cdlemk11u-2N 37907 cdlemk12u-2N 37908 cdlemk20-2N 37910 cdlemk28-3 37926 cdlemk33N 37927 cdlemk34 37928 cdlemk39 37934 cdlemkyyN 37980 |
Copyright terms: Public domain | W3C validator |