![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp23r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp23r | ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3r 1216 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant2 1125 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: ax5seglem6 26283 lshpkrlem5 35268 lplnexllnN 35718 4atexlemutvt 36208 cdlemc5 36349 cdlemd2 36353 cdleme0moN 36379 cdleme3h 36389 cdleme5 36394 cdleme9 36407 cdleme11l 36423 cdleme14 36427 cdleme15c 36430 cdleme16b 36433 cdleme16d 36435 cdleme16e 36436 cdlemednpq 36453 cdleme20bN 36464 cdleme20j 36472 cdleme20l2 36475 cdleme20l 36476 cdleme22cN 36496 cdleme22d 36497 cdleme22e 36498 cdleme22f 36500 cdleme26fALTN 36516 cdleme26f 36517 cdleme26f2ALTN 36518 cdleme26f2 36519 cdleme27a 36521 cdleme32b 36596 cdleme32d 36598 cdleme32f 36600 cdleme39n 36620 cdleme40n 36622 cdlemg2fv2 36754 cdlemg17h 36822 cdlemg27b 36850 cdlemg28b 36857 cdlemg28 36858 cdlemg29 36859 cdlemg33a 36860 cdlemg33d 36863 cdlemk7u-2N 37042 cdlemk11u-2N 37043 cdlemk12u-2N 37044 cdlemk26-3 37060 cdlemk27-3 37061 cdlemkfid3N 37079 cdlemn11c 37363 |
Copyright terms: Public domain | W3C validator |