Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp133 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp133 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp33 1099 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | 3ad2ant1 1082 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: tsmsxp 21958 ax5seglem3 25811 exatleN 34690 3atlem1 34769 3atlem2 34770 3atlem6 34774 4atlem11b 34894 4atlem12b 34897 lplncvrlvol2 34901 dalemuea 34917 dath2 35023 4atexlemex6 35360 cdleme22f2 35635 cdleme22g 35636 cdlemg7aN 35913 cdlemg31c 35987 cdlemg36 36002 cdlemj1 36109 cdlemj2 36110 cdlemk23-3 36190 cdlemk26b-3 36193 |
Copyright terms: Public domain | W3C validator |