![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp1l2 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp1l2 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 1227 | . 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 pmatcollpw2 20777 btwnconn1lem4 32495 linethru 32558 hlrelat3 35193 cvrval3 35194 cvrval4N 35195 2atlt 35220 atbtwnex 35229 1cvratlt 35255 atcvrlln2 35300 atcvrlln 35301 2llnmat 35305 lvolnlelpln 35366 lnjatN 35561 lncmp 35564 cdlemd9 35988 dihord5b 37042 dihmeetALTN 37110 mapdrvallem2 37428 |
Copyright terms: Public domain | W3C validator |