Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp132 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp132 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp32 1098 | . 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: ax5seglem3 25811 3atlem1 34769 3atlem2 34770 3atlem5 34773 2llnjaN 34852 4atlem11b 34894 4atlem12b 34897 lplncvrlvol2 34901 dalemtea 34916 dath2 35023 cdlemblem 35079 dalawlem1 35157 lhpexle3lem 35297 4atexlemex6 35360 cdleme22f2 35635 cdleme22g 35636 cdlemg7aN 35913 cdlemg34 36000 cdlemj1 36109 cdlemk23-3 36190 cdlemk25-3 36192 cdlemk26b-3 36193 |
Copyright terms: Public domain | W3C validator |