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 1201 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑) | |
2 | 1 | 3ad2ant1 1125 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: ax5seglem3 26644 exatleN 36420 3atlem1 36499 3atlem2 36500 3atlem5 36503 2llnjaN 36582 4atlem11b 36624 4atlem12b 36627 lplncvrlvol2 36631 dalemsea 36645 dath2 36753 cdlemblem 36809 dalawlem1 36887 lhpexle3lem 37027 4atexlemex6 37090 cdleme22f2 37363 cdleme22g 37364 cdlemg7aN 37641 cdlemg34 37728 cdlemj1 37837 cdlemk23-3 37918 cdlemk25-3 37920 cdlemk26b-3 37921 cdleml3N 37994 |
Copyright terms: Public domain | W3C validator |