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 1083 | . 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 lshpkrlem5 33419 lplnexllnN 33868 4atexlemutvt 34358 cdlemc5 34500 cdlemd2 34504 cdleme0moN 34530 cdleme3h 34540 cdleme5 34545 cdleme9 34558 cdleme11l 34574 cdleme14 34578 cdleme15c 34581 cdleme16b 34584 cdleme16d 34586 cdleme16e 34587 cdlemednpq 34604 cdleme20bN 34616 cdleme20j 34624 cdleme20l2 34627 cdleme20l 34628 cdleme22cN 34648 cdleme22d 34649 cdleme22e 34650 cdleme22f 34652 cdleme26fALTN 34668 cdleme26f 34669 cdleme26f2ALTN 34670 cdleme26f2 34671 cdleme27a 34673 cdleme32b 34748 cdleme32d 34750 cdleme32f 34752 cdleme39n 34772 cdleme40n 34774 cdlemg2fv2 34906 cdlemg17h 34974 cdlemg27b 35002 cdlemg28b 35009 cdlemg28 35010 cdlemg29 35011 cdlemg33a 35012 cdlemg33d 35015 cdlemk7u-2N 35194 cdlemk11u-2N 35195 cdlemk12u-2N 35196 cdlemk26-3 35212 cdlemk27-3 35213 cdlemkfid3N 35231 cdlemn11c 35516 |
Copyright terms: Public domain | W3C validator |