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 1081 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant1 1075 | 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: ackbij1lem16 8940 lsmcv 18962 nllyrest 21099 axcontlem4 25647 eqlkr 33404 athgt 33760 llncvrlpln2 33861 4atlem11b 33912 2lnat 34088 cdlemblem 34097 pclfinN 34204 lhp2at0nle 34339 4atexlemex6 34378 cdlemd2 34504 cdlemd8 34510 cdleme15a 34579 cdleme16b 34584 cdleme16c 34585 cdleme16d 34586 cdleme20h 34622 cdleme21c 34633 cdleme21ct 34635 cdleme22cN 34648 cdleme23b 34656 cdleme26fALTN 34668 cdleme26f 34669 cdleme26f2ALTN 34670 cdleme26f2 34671 cdleme32le 34753 cdleme35f 34760 cdlemf1 34867 trlord 34875 cdlemg7aN 34931 cdlemg33c0 35008 trlcone 35034 cdlemg44 35039 cdlemg48 35043 cdlemky 35232 cdlemk11ta 35235 cdleml4N 35285 dihmeetlem3N 35612 dihmeetlem13N 35626 mapdpglem32 36012 baerlem3lem2 36017 baerlem5alem2 36018 baerlem5blem2 36019 mzpcong 36557 |
Copyright terms: Public domain | W3C validator |