![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp21r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp21r | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1r 1212 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant2 1125 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ 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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: modexp 13318 segconeu 32707 4atlem10 35760 lplncvrlvol2 35769 4atex 36230 4atex2-0cOLDN 36234 cdleme0moN 36379 cdleme16e 36436 cdleme17d1 36443 cdleme18d 36449 cdleme19d 36460 cdleme20f 36468 cdleme20g 36469 cdleme21ct 36483 cdleme22aa 36493 cdleme22cN 36496 cdleme22d 36497 cdleme22e 36498 cdleme22eALTN 36499 cdleme26e 36513 cdleme32e 36599 cdleme32f 36600 cdlemg4 36771 cdlemg18d 36835 cdlemg18 36836 cdlemg19a 36837 cdlemg19 36838 cdlemg21 36840 cdlemg33b0 36855 cdlemk5 36990 cdlemk6 36991 cdlemk7 37002 cdlemk11 37003 cdlemk12 37004 cdlemk21N 37027 cdlemk20 37028 cdlemk28-3 37062 cdlemk34 37064 cdlemkfid3N 37079 cdlemk55u1 37119 |
Copyright terms: Public domain | W3C validator |