![]() |
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 1244 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant2 1128 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ 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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: ax5seglem6 26034 lshpkrlem5 34922 lplnexllnN 35372 4atexlemutvt 35862 cdlemc5 36004 cdlemd2 36008 cdleme0moN 36034 cdleme3h 36044 cdleme5 36049 cdleme9 36062 cdleme11l 36078 cdleme14 36082 cdleme15c 36085 cdleme16b 36088 cdleme16d 36090 cdleme16e 36091 cdlemednpq 36108 cdleme20bN 36119 cdleme20j 36127 cdleme20l2 36130 cdleme20l 36131 cdleme22cN 36151 cdleme22d 36152 cdleme22e 36153 cdleme22f 36155 cdleme26fALTN 36171 cdleme26f 36172 cdleme26f2ALTN 36173 cdleme26f2 36174 cdleme27a 36176 cdleme32b 36251 cdleme32d 36253 cdleme32f 36255 cdleme39n 36275 cdleme40n 36277 cdlemg2fv2 36409 cdlemg17h 36477 cdlemg27b 36505 cdlemg28b 36512 cdlemg28 36513 cdlemg29 36514 cdlemg33a 36515 cdlemg33d 36518 cdlemk7u-2N 36697 cdlemk11u-2N 36698 cdlemk12u-2N 36699 cdlemk26-3 36715 cdlemk27-3 36716 cdlemkfid3N 36734 cdlemn11c 37019 |
Copyright terms: Public domain | W3C validator |