Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp123 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp123 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp23 1096 | . 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 axpasch 25821 exatleN 34690 ps-2b 34768 3atlem1 34769 3atlem2 34770 3atlem4 34772 3atlem5 34773 3atlem6 34774 2llnjaN 34852 2llnjN 34853 4atlem12b 34897 2lplnja 34905 2lplnj 34906 dalemrea 34914 dath2 35023 lneq2at 35064 osumcllem7N 35248 cdleme26ee 35648 cdlemg35 36001 cdlemg36 36002 cdlemj1 36109 cdlemk23-3 36190 cdlemk25-3 36192 cdlemk26b-3 36193 cdlemk27-3 36195 cdlemk28-3 36196 cdleml3N 36266 |
Copyright terms: Public domain | W3C validator |