| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp12r | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp12r | ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp2r 1201 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
| 2 | 1 | 3ad2ant1 1134 | 1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: ackbij1lem16 10274 lsmcv 21143 nllyrest 23494 axcontlem4 28982 eqlkr 39100 athgt 39458 llncvrlpln2 39559 4atlem11b 39610 2lnat 39786 cdlemblem 39795 pclfinN 39902 lhp2at0nle 40037 4atexlemex6 40076 cdlemd2 40201 cdlemd8 40207 cdleme15a 40276 cdleme16b 40281 cdleme16c 40282 cdleme16d 40283 cdleme20h 40318 cdleme21c 40329 cdleme21ct 40331 cdleme22cN 40344 cdleme23b 40352 cdleme26fALTN 40364 cdleme26f 40365 cdleme26f2ALTN 40366 cdleme26f2 40367 cdleme32le 40449 cdleme35f 40456 cdlemf1 40563 trlord 40571 cdlemg7aN 40627 cdlemg33c0 40704 trlcone 40730 cdlemg44 40735 cdlemg48 40739 cdlemky 40928 cdlemk11ta 40931 cdleml4N 40981 dihmeetlem3N 41307 dihmeetlem13N 41321 mapdpglem32 41707 baerlem3lem2 41712 baerlem5alem2 41713 baerlem5blem2 41714 mzpcong 42984 iscnrm3rlem8 48844 |
| Copyright terms: Public domain | W3C validator |