![]() |
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 1206 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜓) | |
2 | 1 | 3ad2ant1 1132 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: ax5seglem3 28961 axpasch 28971 exatleN 39387 ps-2b 39465 3atlem1 39466 3atlem2 39467 3atlem4 39469 3atlem5 39470 3atlem6 39471 2llnjaN 39549 4atlem12b 39594 2lplnja 39602 dalemqea 39610 dath2 39720 lneq2at 39761 llnexchb2 39852 dalawlem1 39854 lhpexle3lem 39994 cdleme26ee 40343 cdlemg34 40695 cdlemg35 40696 cdlemg36 40697 cdlemj1 40804 cdlemj2 40805 cdlemk23-3 40885 cdlemk25-3 40887 cdlemk26b-3 40888 cdlemk26-3 40889 cdleml3N 40961 iscnrm3llem2 48747 |
Copyright terms: Public domain | W3C validator |