![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp121 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp121 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp21 1264 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜑) | |
2 | 1 | 3ad2ant1 1164 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1108 |
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 199 df-an 386 df-3an 1110 |
This theorem is referenced by: ax5seglem3 26168 axpasch 26178 exatleN 35425 ps-2b 35503 3atlem1 35504 3atlem2 35505 3atlem4 35507 3atlem5 35508 3atlem6 35509 2llnjaN 35587 4atlem12b 35632 2lplnja 35640 dalempea 35647 dath2 35758 lneq2at 35799 llnexchb2 35890 dalawlem1 35892 osumcllem7N 35983 lhpexle3lem 36032 cdleme26ee 36381 cdlemg34 36733 cdlemg36 36735 cdlemj1 36842 cdlemj2 36843 cdlemk23-3 36923 cdlemk25-3 36925 cdlemk26b-3 36926 cdlemk26-3 36927 cdlemk27-3 36928 cdleml3N 36999 |
Copyright terms: Public domain | W3C validator |