![]() |
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 1198 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant1 1131 | 1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 206 df-an 396 df-3an 1087 |
This theorem is referenced by: ackbij1lem16 10244 lsmcv 21011 nllyrest 23364 axcontlem4 28752 eqlkr 38495 athgt 38853 llncvrlpln2 38954 4atlem11b 39005 2lnat 39181 cdlemblem 39190 pclfinN 39297 lhp2at0nle 39432 4atexlemex6 39471 cdlemd2 39596 cdlemd8 39602 cdleme15a 39671 cdleme16b 39676 cdleme16c 39677 cdleme16d 39678 cdleme20h 39713 cdleme21c 39724 cdleme21ct 39726 cdleme22cN 39739 cdleme23b 39747 cdleme26fALTN 39759 cdleme26f 39760 cdleme26f2ALTN 39761 cdleme26f2 39762 cdleme32le 39844 cdleme35f 39851 cdlemf1 39958 trlord 39966 cdlemg7aN 40022 cdlemg33c0 40099 trlcone 40125 cdlemg44 40130 cdlemg48 40134 cdlemky 40323 cdlemk11ta 40326 cdleml4N 40376 dihmeetlem3N 40702 dihmeetlem13N 40716 mapdpglem32 41102 baerlem3lem2 41107 baerlem5alem2 41108 baerlem5blem2 41109 mzpcong 42305 iscnrm3rlem8 47879 |
Copyright terms: Public domain | W3C validator |