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 1087 | . 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 axpasch 25621 exatleN 33708 ps-2b 33786 3atlem1 33787 3atlem2 33788 3atlem4 33790 3atlem5 33791 3atlem6 33792 2llnjaN 33870 4atlem12b 33915 2lplnja 33923 dalempea 33930 dath2 34041 lneq2at 34082 llnexchb2 34173 dalawlem1 34175 osumcllem7N 34266 lhpexle3lem 34315 cdleme26ee 34666 cdlemg34 35018 cdlemg36 35020 cdlemj1 35127 cdlemj2 35128 cdlemk23-3 35208 cdlemk25-3 35210 cdlemk26b-3 35211 cdlemk26-3 35212 cdlemk27-3 35213 cdleml3N 35284 |
Copyright terms: Public domain | W3C validator |