Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp122 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp122 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp22 1209 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜓) | |
2 | 1 | 3ad2ant1 1135 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: ax5seglem3 27054 axpasch 27064 exatleN 37192 ps-2b 37270 3atlem1 37271 3atlem2 37272 3atlem4 37274 3atlem5 37275 3atlem6 37276 2llnjaN 37354 4atlem12b 37399 2lplnja 37407 dalemqea 37415 dath2 37525 lneq2at 37566 llnexchb2 37657 dalawlem1 37659 lhpexle3lem 37799 cdleme26ee 38148 cdlemg34 38500 cdlemg35 38501 cdlemg36 38502 cdlemj1 38609 cdlemj2 38610 cdlemk23-3 38690 cdlemk25-3 38692 cdlemk26b-3 38693 cdlemk26-3 38694 cdleml3N 38766 iscnrm3llem2 45963 |
Copyright terms: Public domain | W3C validator |