![]() |
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 1195 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant2 1131 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: modexp 14255 segconeu 35835 4atlem10 39305 lplncvrlvol2 39314 4atex 39775 4atex2-0cOLDN 39779 cdleme0moN 39924 cdleme16e 39981 cdleme17d1 39988 cdleme18d 39994 cdleme19d 40005 cdleme20f 40013 cdleme20g 40014 cdleme21ct 40028 cdleme22aa 40038 cdleme22cN 40041 cdleme22d 40042 cdleme22e 40043 cdleme22eALTN 40044 cdleme26e 40058 cdleme32e 40144 cdleme32f 40145 cdlemg4 40316 cdlemg18d 40380 cdlemg18 40381 cdlemg19a 40382 cdlemg19 40383 cdlemg21 40385 cdlemg33b0 40400 cdlemk5 40535 cdlemk6 40536 cdlemk7 40547 cdlemk11 40548 cdlemk12 40549 cdlemk21N 40572 cdlemk20 40573 cdlemk28-3 40607 cdlemk34 40609 cdlemkfid3N 40624 cdlemk55u1 40664 |
Copyright terms: Public domain | W3C validator |