![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp1l1 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp1l1 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1225 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant1 1127 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 385 df-3an 1074 |
This theorem is referenced by: mapxpen 8283 lsmcv 19335 archiabl 30053 trisegint 32433 linethru 32558 hlrelat3 35193 cvrval3 35194 cvrval4N 35195 2atlt 35220 atbtwnex 35229 1cvratlt 35255 atcvrlln2 35300 atcvrlln 35301 2llnmat 35305 lplnexllnN 35345 lvolnlelpln 35366 lnjatN 35561 lncvrat 35563 lncmp 35564 cdlemd9 35988 dihord5b 37042 dihmeetALTN 37110 dih1dimatlem0 37111 mapdrvallem2 37428 |
Copyright terms: Public domain | W3C validator |