| 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 8092 mapxpen 9071 hash7g 14409 lsmcv 21096 ltslpss 27904 archiabl 33280 trisegint 36222 linethru 36347 hlrelat3 39672 cvrval3 39673 cvrval4N 39674 2atlt 39699 atbtwnex 39708 1cvratlt 39734 atcvrlln2 39779 atcvrlln 39780 2llnmat 39784 lplnexllnN 39824 lvolnlelpln 39845 lnjatN 40040 lncvrat 40042 lncmp 40043 cdlemd9 40466 dihord5b 41519 dihmeetALTN 41587 dih1dimatlem0 41588 mapdrvallem2 41905 grumnudlem 44526 |
| Copyright terms: Public domain | W3C validator |