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 1090 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑) | |
2 | 1 | 3ad2ant1 1075 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ 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: ax5seglem3 25611 exatleN 33708 3atlem1 33787 3atlem2 33788 3atlem5 33791 2llnjaN 33870 4atlem11b 33912 4atlem12b 33915 lplncvrlvol2 33919 dalemsea 33933 dath2 34041 cdlemblem 34097 dalawlem1 34175 lhpexle3lem 34315 4atexlemex6 34378 cdleme22f2 34653 cdleme22g 34654 cdlemg7aN 34931 cdlemg34 35018 cdlemj1 35127 cdlemk23-3 35208 cdlemk25-3 35210 cdlemk26b-3 35211 cdleml3N 35284 |
Copyright terms: Public domain | W3C validator |