| 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 1192 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | |
| 2 | 1 | 3ad2ant1 1133 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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: poxp3 8131 mapxpen 9112 hash7g 14457 lsmcv 21057 sltlpss 27825 archiabl 33158 trisegint 36011 linethru 36136 hlrelat3 39401 cvrval3 39402 cvrval4N 39403 2atlt 39428 atbtwnex 39437 1cvratlt 39463 atcvrlln2 39508 atcvrlln 39509 2llnmat 39513 lplnexllnN 39553 lvolnlelpln 39574 lnjatN 39769 lncvrat 39771 lncmp 39772 cdlemd9 40195 dihord5b 41248 dihmeetALTN 41316 dih1dimatlem0 41317 mapdrvallem2 41634 grumnudlem 44267 |
| Copyright terms: Public domain | W3C validator |