![]() |
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 1263 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant1 1169 | 1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 |
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 1115 |
This theorem is referenced by: ackbij1lem16 9371 lsmcv 19500 nllyrest 21659 axcontlem4 26265 eqlkr 35173 athgt 35530 llncvrlpln2 35631 4atlem11b 35682 2lnat 35858 cdlemblem 35867 pclfinN 35974 lhp2at0nle 36109 4atexlemex6 36148 cdlemd2 36273 cdlemd8 36279 cdleme15a 36348 cdleme16b 36353 cdleme16c 36354 cdleme16d 36355 cdleme20h 36390 cdleme21c 36401 cdleme21ct 36403 cdleme22cN 36416 cdleme23b 36424 cdleme26fALTN 36436 cdleme26f 36437 cdleme26f2ALTN 36438 cdleme26f2 36439 cdleme32le 36521 cdleme35f 36528 cdlemf1 36635 trlord 36643 cdlemg7aN 36699 cdlemg33c0 36776 trlcone 36802 cdlemg44 36807 cdlemg48 36811 cdlemky 37000 cdlemk11ta 37003 cdleml4N 37053 dihmeetlem3N 37379 dihmeetlem13N 37393 mapdpglem32 37779 baerlem3lem2 37784 baerlem5alem2 37785 baerlem5blem2 37786 mzpcong 38381 |
Copyright terms: Public domain | W3C validator |