![]() |
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 1171 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant1 1113 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: mapxpen 8479 lsmcv 19635 archiabl 30499 trisegint 33016 linethru 33141 hlrelat3 35999 cvrval3 36000 cvrval4N 36001 2atlt 36026 atbtwnex 36035 1cvratlt 36061 atcvrlln2 36106 atcvrlln 36107 2llnmat 36111 lplnexllnN 36151 lvolnlelpln 36172 lnjatN 36367 lncvrat 36369 lncmp 36370 cdlemd9 36793 dihord5b 37846 dihmeetALTN 37914 dih1dimatlem0 37915 mapdrvallem2 38232 grumnudlem 40002 |
Copyright terms: Public domain | W3C validator |