|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simp131 | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) | 
| Ref | Expression | 
|---|---|
| simp131 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simp31 1209 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑) | |
| 2 | 1 | 3ad2ant1 1133 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: ax5seglem3 28947 exatleN 39407 3atlem1 39486 3atlem2 39487 3atlem5 39490 2llnjaN 39569 4atlem11b 39611 4atlem12b 39614 lplncvrlvol2 39618 dalemsea 39632 dath2 39740 cdlemblem 39796 dalawlem1 39874 lhpexle3lem 40014 4atexlemex6 40077 cdleme22f2 40350 cdleme22g 40351 cdlemg7aN 40628 cdlemg34 40715 cdlemj1 40824 cdlemk23-3 40905 cdlemk25-3 40907 cdlemk26b-3 40908 cdleml3N 40981 | 
| Copyright terms: Public domain | W3C validator |